diff --git a/tests/lean/run/evalconst.lean b/tests/lean/run/evalconst.lean index 79465c6367..f054de2a8f 100644 --- a/tests/lean/run/evalconst.lean +++ b/tests/lean/run/evalconst.lean @@ -9,3 +9,13 @@ IO.println $ env.evalConst Nat `x; pure () #eval tst + +def f (x : Nat) := x + 1 + +unsafe def tst2 : MetaIO Unit := do +env ← MetaIO.getEnv; +f ← liftM $ IO.ofExcept $ env.evalConst (Nat → Nat) `f; +IO.println $ (f 10); +pure () + +#eval tst2