10 Minute Vim!

Darkest Proof: Day 1

· Read in about 1 min · (210 Words)

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.

STEVE SHOGREN

software developer, manager, author, speaker

BOOKS:

POSTS FOR:

CATEGORIES