Good ideas and conversation. No ads, no tracking. Login or Take a Tour!
For anyone who happens to read this and gets interested in Coq, I found that my understanding of the inner workings of it—and thus my ability to do proofs—was hugely aided by running (equivalently) "Show Proof." during proof-editing mode, or "Print <X>." where <X> is the proof object after it is defined. Thus one learns that (forall n:nat, n + 0 = n) is inhabited by nat_ind (fun n => n + 0 = n)
eq_refl
(fun n0 IH => eq_ind_r (fun n1 => S n1 = S n0) eq_refl IH)
n