lean2/tests/lean/run/class1.lean

import standard
using num pair

definition H : inhabited (Prop × num × (num → num)) := _

(*
print(get_env():find("H"):value())
*)
-												feat(frontends/lean/elaborator): add class instance elaboration

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

											
										
										
											2014-07-04 15:45:50 -07:00
+								import standard
-												feat(frontends/lean/builtin_cmds): allow many namespaces in the same 'using' command

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

											
										
										
											2014-07-07 14:53:06 -07:00
+								using num pair
-												feat(frontends/lean/elaborator): add class instance elaboration

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

											
										
										
											2014-07-04 15:45:50 -07:00
-												refactor(*): rename Bool to Prop

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

											
										
										
											2014-07-22 09:43:18 -07:00
+								definition H : inhabited (Prop × num × (num → num)) := _
-												feat(frontends/lean/elaborator): add class instance elaboration

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

											
										
										
											2014-07-04 15:45:50 -07:00
 								(*
 								print(get_env():find("H"):value())
 								*)