diff --git a/test/issues/26.lean b/test/issues/26.lean new file mode 100644 index 00000000..b1f28b27 --- /dev/null +++ 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})