lean2/tests/lean/run/class2.lean

import standard
using num prod

theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
:= _

(*
print(get_env():find("H"):value())
*)
-												feat(frontends/lean/elaborator): use local declarations as class instances

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-05 01:03:13 +00:00
+								import standard
-												fix(tests/lean/run): adjust test to changes in the library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-15 20:27:18 +00:00
+								using num prod
-												feat(frontends/lean/elaborator): use local declarations as class instances

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-05 01:03:13 +00:00
-												refactor(*): rename Bool to Prop

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-22 16:43:18 +00:00
+								theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
-												feat(frontends/lean/elaborator): use local declarations as class instances

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-05 01:03:13 +00:00
+								:= _
 								(*
 								print(get_env():find("H"):value())
 								*)