Skip to content

Instantly share code, notes, and snippets.

@Steffan153

Steffan153/B4B_smarter.v

Forked from DonaldKellett/B4B_smarter.v
Last active October 31, 2019 17:57
Show Gist options
  • Save Steffan153/6f093665fba8da858ac3eddb185f91a9 to your computer and use it in GitHub Desktop.
Save Steffan153/6f093665fba8da858ac3eddb185f91a9 to your computer and use it in GitHub Desktop.
Download ZIP
A formal proof that @Blind4Basics is getting smarter every day
Raw
B4B_smarter.v
(*
* A formal proof that @Blind4Basics is getting smarter every day
* Special thanks to @AwelEshetu for raising this question and
* @Steffan153 for challenging me into making this compile ;-)
*)
Definition Blind4Basics (_ _ _ _ _ : unit) := True.
Definition is := tt.
Definition getting := tt.
Definition smarter := tt.
Definition every := tt.
Definition day := tt.
Tactic Notation "well" ident(duh) ident(obviously) ident(unlike) ident(awel) ident(esethu) := easy.
Theorem B4B_smarter : Blind4Basics is getting smarter every day.
Proof.
well duh obviously unlike awel esethu.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment