diff --git a/tests/lean/run/e6.lean b/tests/lean/run/e6.lean new file mode 100644 index 000000000..6c9d65c10 --- /dev/null +++ b/tests/lean/run/e6.lean @@ -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 + +