From d22abd85dd6cfefe3a6125f59c7e5af6ddbfe233 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jan 2020 11:02:38 -0800
Subject: [PATCH] test: minimal repro for evalConst crash

---
 tests/lean/run/evalconst.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

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