Created
October 31, 2019 15:19
-
-
Save DonaldKellett/3cbe487203eeb106b38d95579e9a46a1 to your computer and use it in GitHub Desktop.
A formal proof that @Blind4Basics is getting smarter every day
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* | |
| * 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