diff --git a/tests/lean/run/695e.lean b/tests/lean/run/695e.lean new file mode 100644 index 0000000000..ab1ad4c1b5 --- /dev/null +++ b/tests/lean/run/695e.lean @@ -0,0 +1,3 @@ +open nat +example (n : ℕ) : n + 1 = succ n := +by rewrite [