Skip to content

Instantly share code, notes, and snippets.

@DonaldKellett

DonaldKellett/B4B_smarter.v

Created October 31, 2019 15:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save DonaldKellett/3cbe487203eeb106b38d95579e9a46a1 to your computer and use it in GitHub Desktop.
Save DonaldKellett/3cbe487203eeb106b38d95579e9a46a1 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(you) := easy.
Theorem B4B_smarter : Blind4Basics is getting smarter every day.
Proof.
well duh obviously unlike you.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment