Also worthy of note is Coq in a hurry where it goes on a little more about proofs on inductive proof principles by using the naturals and lists as examples. I used it when preparing my “Type theory and Coq” exam and things were rather pleasant after that except for some nasty functions which I couldn’t get to typecheck and I had to resort to Program Fixpoint to delay some proofs.

Also worthy of note is Coq in a hurry where it goes on a little more about proofs on inductive proof principles by using the naturals and lists as examples. I used it when preparing my “Type theory and Coq” exam and things were rather pleasant after that except for some nasty functions which I couldn’t get to typecheck and I had to resort to

Program Fixpointto delay some proofs.