test(tests/lean/run): add simple overloading test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
2d2f23cda6
commit
da6e92787a
1 changed files with 33 additions and 0 deletions
33
tests/lean/run/e6.lean
Normal file
33
tests/lean/run/e6.lean
Normal file
|
@ -0,0 +1,33 @@
|
||||||
|
|
||||||
|
precedence `+`:65
|
||||||
|
|
||||||
|
namespace nat
|
||||||
|
variable nat : Type.{1}
|
||||||
|
variable add : nat → nat → nat
|
||||||
|
infixl + := add
|
||||||
|
end
|
||||||
|
|
||||||
|
namespace int
|
||||||
|
using nat (nat)
|
||||||
|
variable int : Type.{1}
|
||||||
|
variable add : int → int → int
|
||||||
|
infixl + := add
|
||||||
|
variable of_nat : nat → int
|
||||||
|
coercion of_nat
|
||||||
|
end
|
||||||
|
|
||||||
|
using int
|
||||||
|
using nat
|
||||||
|
|
||||||
|
variables n m : nat
|
||||||
|
variables i j : int
|
||||||
|
|
||||||
|
check n + m
|
||||||
|
check i + j
|
||||||
|
check i + n
|
||||||
|
check i + n + n + n + n + n + n + n + n + n + n + n +
|
||||||
|
n + n + n + n + n + n + n + n + n + n + n + n +
|
||||||
|
n + n + n + n + n + n + n + n + n + n + n + n +
|
||||||
|
n + n + n + n + n + n + n + n + n + n + n + n
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue