Apr 21, 2014 · 7:00 PM
Let's go through the exercises in the Induction chapter of SF, and then get together and discuss them.
Induction lets us prove some theorems that aren't totally trivial, so Coq starts to get a little more fun.
As I think we agreed this evening, interaction with Coq can be a little mysterious. Don't stress out! I suspect we're learning something even when we're just flailing around, so feel free to flail away. And post a message on meetup or the Google group if you get stuck on something.