From 3df7f35dd0416fc376579ade49efae3b68ca4e38 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Mar 2020 13:38:06 -0700
Subject: [PATCH] test: kernel isDefEq support for Nat operations

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

diff --git a/tests/lean/run/kernel2.lean b/tests/lean/run/kernel2.lean
new file mode 100644
index 0000000000..821b2f31ed
--- /dev/null
+++ b/tests/lean/run/kernel2.lean
@@ -0,0 +1,36 @@
+import Init.Lean
+open Lean
+
+def checkDefEq (a b : Name) : MetaIO Unit := do
+env ← MetaIO.getEnv;
+let a := mkConst a;
+let b := mkConst b;
+let r := Kernel.isDefEq env {} a b;
+IO.println (toString a ++ " =?= " ++ toString b ++ " := " ++ toString r)
+
+def whnf (a : Name) : MetaIO Unit := do
+env ← MetaIO.getEnv;
+let a := mkConst a;
+let r := Kernel.whnf env {} a;
+IO.println (toString a ++ " ==> " ++ toString r)
+
+def fact : Nat → Nat
+| 0     => 1
+| (n+1) => (n+1)*fact n
+
+def c1 := 30000000000 + 10000000000
+def c2 := 40000000000
+def c3 := fact 10
+def v1  := 3628800
+def v2  := 3628801
+#eval whnf `c3
+#eval checkDefEq `c3 `v1
+#eval checkDefEq `c3 `v2
+#eval checkDefEq `c1 `c2
+
+set_option pp.all true
+
+def c4 := decide (100000000 < 20000000000)
+
+#eval whnf `c4
+#eval checkDefEq `c4 `Bool.true