test: minimal repro for evalConst crash

This commit is contained in:
Leonardo de Moura 2020-01-01 11:02:38 -08:00
parent 61403b556d
commit d22abd85dd

View file

@ -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