test(lean/run): add notation test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
08845be2fc
commit
3bb53810c5
1 changed files with 20 additions and 0 deletions
20
tests/lean/run/n4.lean
Normal file
20
tests/lean/run/n4.lean
Normal file
|
@ -0,0 +1,20 @@
|
|||
definition [inline] Bool : Type.{1} := Type.{0}
|
||||
section
|
||||
variable N : Type.{1}
|
||||
variables a b c : N
|
||||
variable and : Bool → Bool → Bool
|
||||
infixr `∧` 35 := and
|
||||
variable le : N → N → Bool
|
||||
variable lt : N → N → Bool
|
||||
precedence `≤`:50
|
||||
precedence `<`:50
|
||||
infixl ≤ := le
|
||||
infixl < := lt
|
||||
check a ≤ b
|
||||
definition T : Bool := a ≤ b
|
||||
check T
|
||||
end
|
||||
check T
|
||||
(*
|
||||
print(get_env():find("T"):value())
|
||||
*)
|
Loading…
Reference in a new issue