test: add new_frontend command test
This commit is contained in:
parent
e0ae6068d4
commit
4b37c5ad04
1 changed files with 17 additions and 0 deletions
17
tests/lean/run/newfrontend1.lean
Normal file
17
tests/lean/run/newfrontend1.lean
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
def x := 1
|
||||
|
||||
new_frontend
|
||||
|
||||
#check x
|
||||
|
||||
variables {α : Type}
|
||||
|
||||
def f (a : α) : α :=
|
||||
a
|
||||
|
||||
def tst (xs : List Nat) : Nat :=
|
||||
xs.foldl (init := 10) (· + ·)
|
||||
|
||||
#check tst [1, 2, 3]
|
||||
|
||||
#check tst
|
||||
Loading…
Add table
Reference in a new issue