lean2/tests/lean/interactive/coe.lean

import data.int
open int

protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
take (a b : ℤ), _

constant n : nat
constant i : int
check n + i
-												fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151

											
										
										
											2014-09-09 12:46:55 -07:00
+								import data.int
 								open int
-												refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.

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

											
										
										
											2014-09-19 15:04:52 -07:00
+								protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
-												refactor(library): replace decidable_eq with abbreviation

											
										
										
											2014-09-09 16:07:07 -07:00
+								take (a b : ℤ), _
-												fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151

											
										
										
											2014-09-09 12:46:55 -07:00
-												refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands

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

											
										
										
											2014-10-02 16:20:52 -07:00
+								constant n : nat
 								constant i : int
-												fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151

											
										
										
											2014-09-09 12:46:55 -07:00
+								check n + i