Day one working through Software Foundations with Coq. Since I like to rant, and I love Darkest Dungeon, ENTER THE DARKEST PROOF. (Please don’t sue me!)
Precise Syntax
I copied a sample from the book by hand, but it always caused Company-Coq to go into an infinite loop. I copied it again. Same deal.
This isn’t my first rodeo, I’ve seen all sorts of syntax rules and such. But alas, it still fails.
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b.
{ destruct c.
{ reflexivity.}
{ reflexivity.} }
{ destruct c.
{ reflexivity.}
{ reflexivity.} }
Qed.
Where the heck is it? I am losing my mind for 20 minutes looking back and forth
trying to figure out what I am missing. I seek the advice of a friend, he
suggests stepping line-by-line with C-cC-n.
It fails on one line.
Wait.
Thats…
But…
NO!!!!!
Coq is WHITE-SPACE SENSITIVE?!
YEP! I add that space in, and it works fine!
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b.
{ destruct c.
{ reflexivity. }
{ reflexivity. } }
{ destruct c.
{ reflexivity. }
{ reflexivity. } }
Qed.
