michael/lean2 - Forgejo: Beyond coding. We forge.

michael/lean2

5 lines

164 B

Text

Raw Permalink Normal View History

-												feat(frontends/lean): use nice names for meta-variables when executing `check c` and `c` is a constant

											
										
										
											2014-10-24 15:19:36 +00:00
+								and.intro : ?a → ?b → ?a ∧ ?b
 								or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
 								eq : ?A → ?A → Prop
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								eq.rec : ?C ?a → (Π {a}, ?a = a → ?C a)