From 67c88f12bd5d892764e013e25fbc2895ed97682c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Nov 2019 09:05:38 -0800
Subject: [PATCH] test: add basic test

---
 tests/lean/run/meta2.lean | 42 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 tests/lean/run/meta2.lean

diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
new file mode 100644
index 0000000000..a9a0b173a4
--- /dev/null
+++ b/tests/lean/run/meta2.lean
@@ -0,0 +1,42 @@
+import Init.Lean.Meta
+open Lean
+open Lean.Meta
+
+def dbgOpt : Options :=
+let opt : Options := {};
+let opt := opt.setBool `trace.Meta.debug true;
+let opt := opt.setBool `trace.Meta.isDefEq true;
+let opt := opt.setBool `trace.Meta.isDefEq true;
+opt
+
+def print (msg : MessageData) : MetaM Unit :=
+trace! `Meta.debug msg
+
+def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit :=
+do env ← importModules $ mods.map $ fun m => {module := m};
+   match x { config := { opts := opts } } { env := env } with
+   | EStateM.Result.ok _ s    => do
+     s.traceState.traces.forM $ fun m => IO.println $ format m;
+     pure ()
+   | EStateM.Result.error err _ => throw (IO.userError (toString err))
+
+def tst1 : MetaM Unit :=
+do print "----- tst1 -----";
+   let nat := mkConst `Nat;
+   mvar ← mkFreshExprMVar nat;
+   isExprDefEq mvar (mkNatLit 10);
+   isExprDefEq mvar (mkNatLit 10);
+   pure ()
+
+#eval run [`Init.Data.Nat] tst1
+
+def tst2 : MetaM Unit :=
+do print "----- tst2 -----";
+   let nat  := mkConst `Nat;
+   let succ := mkConst `Nat.succ;
+   mvar ← mkFreshExprMVar nat;
+   isExprDefEq (mkApp succ mvar) (mkApp succ (mkNatLit 10));
+   isExprDefEq mvar (mkNatLit 10);
+   pure ()
+
+#eval run [`Init.Data.Nat] tst2