From ecfc01b2d08e2762e545ee1c4145cd3e928c5b37 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Jun 2015 13:10:15 -0700
Subject: [PATCH] test(tests/lean/run): add test for `<d` notation

see issue #695

remark: we have to fix the tutorial the ASCII notation for fold is `<d`
instead of `<D`
---
 tests/lean/run/695e.lean | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 tests/lean/run/695e.lean

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 [<d n+1]