feat(frontends/lean): extend parser: rewrite "fold" step

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -55,6 +55,12 @@ static expr parse_rewrite_unfold(parser & p) {
 expr parse_rewrite_element(parser & p) {
     if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk()))
         return parse_rewrite_unfold(p);
+    if (p.curr_is_token(get_down_tk())) {
+        p.next();
+        expr e = p.parse_expr();
+        location loc = parse_tactic_location(p);
+        return mk_rewrite_fold(e, loc);
+    }
     bool symm = false;
     if (p.curr_is_token(get_sub_tk())) {
         p.next();

src/frontends/lean/tokens.cpp

@@ -27,6 +27,7 @@ static name * g_rangle       = nullptr;
 static name * g_triangle     = nullptr;
 static name * g_caret        = nullptr;
 static name * g_up           = nullptr;
+static name * g_down         = nullptr;
 static name * g_bar          = nullptr;
 static name * g_comma        = nullptr;
 static name * g_add          = nullptr;
@@ -142,6 +143,7 @@ void initialize_tokens() {
     g_triangle     = new name("▸");
     g_caret        = new name("^");
     g_up           = new name("↑");
+    g_down         = new name("<d");
     g_bar          = new name("|");
     g_comma        = new name(",");
     g_add          = new name("+");
@@ -336,6 +338,7 @@ void finalize_tokens() {
     delete g_triangle;
     delete g_caret;
     delete g_up;
+    delete g_down;
     delete g_rbracket;
     delete g_lbracket;
     delete g_rdcurly;
@@ -362,6 +365,7 @@ name const & get_rangle_tk() { return *g_rangle; }
 name const & get_triangle_tk() { return *g_triangle; }
 name const & get_caret_tk() { return *g_caret; }
 name const & get_up_tk() { return *g_up; }
+name const & get_down_tk() { return *g_down; }
 name const & get_lparen_tk() { return *g_lparen; }
 name const & get_rparen_tk() { return *g_rparen; }
 name const & get_llevel_curly_tk() { return *g_llevel_curly; }

src/frontends/lean/tokens.h

@@ -29,6 +29,7 @@ name const & get_rangle_tk();
 name const & get_triangle_tk();
 name const & get_caret_tk();
 name const & get_up_tk();
+name const & get_down_tk();
 name const & get_bar_tk();
 name const & get_comma_tk();
 name const & get_add_tk();

tests/lean/run/rewriter17.lean

@@ -0,0 +1,9 @@
+open nat
+
+definition foo [irreducible] (x : nat) := x + 1
+
+example (a b : nat) (H : foo a = b) : a + 1 = b :=
+begin
+  rewrite ↓foo a,
+  exact H
+end

tests/lean/run/rewriter18.lean

@@ -0,0 +1,10 @@
+import algebra.ring
+open algebra
+
+definition foo {A : Type} [s : monoid A] (a : A) :=
+a * a
+
+example {A : Type} [s : comm_ring A] (a b : A) (H : foo a = a) : a * a = a :=
+begin
+  rewrite [↓foo a, H]
+end