test for #26

lecopivo · Oct 25, 2023 · 4ac0357 · 4ac0357
1 parent 387e536
commit 4ac0357
Showing 1 changed file with 23 additions and 0 deletions.
diff --git a/test/issues/26.lean b/test/issues/26.lean
@@ -0,0 +1,23 @@
+import SciLean
+
+
+variable (a : Nat)
+
+/- expected
+info: let x := a + a;
+a + (a + x) : ℕ
+-/
+
+/--
+info: a +
+  let x := a + a;
+  a + x : ℕ
+-/
+#guard_msgs in
+#check 
+  (a + 
+    (a + 
+    let x := a + a
+    x))
+  rewrite_by
+    lsimp (config := {zeta := false, singlePass := true})