diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean new file mode 100644 index 0000000000..2ec5d919b6 --- /dev/null +++ b/tests/lean/run/newfrontend1.lean @@ -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