From f0e2a3cfa461b436be3ebae7daf9bf12d8e71f11 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Feb 2020 20:37:37 -0800
Subject: [PATCH] chore: add small test

---
 tests/lean/run/meta2.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 843f5a070a..e2b1886b74 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -554,3 +554,15 @@ check r;
 pure ()
 
 #eval tst33
+
+def tst34 : MetaM Unit := do
+print "----- tst33 -----";
+let type := mkSort levelOne;
+withLocalDecl `α type BinderInfo.default $ fun α => do
+  m ← mkFreshExprMVar α;
+  t ← approxDefEq $ mkLambda #[α] (mkArrow m m);
+  print t;
+  pure ()
+
+set_option pp.purify_metavars false
+#eval tst34