From 16ec651269b0f0e864138c9dc88b5791ff67480a Mon Sep 17 00:00:00 2001
From: jmkjmt <95419287+jmkjmt@users.noreply.github.com>
Date: Tue, 11 Nov 2025 15:18:10 +0900
Subject: [PATCH] Add direction option to rewrite tactic in README

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index b5caab9..fb02678 100644
--- a/README.md
+++ b/README.md
@@ -114,7 +114,7 @@ forall (nat1:nat), add (nat1) (0) = nat1
                   | "assert" <prop>
                   | "simpl"
                   | "simpl in" <target_label> 
-                  | "rewrite" <rewrite_label> "in" <target_label> "at" <loc>
+                  | "rewrite" <direction> <rewrite_label> "in" <target_label> "at" <loc>
                   | "induction" <var>
                   | "case" <expr>
                   | "intro" <var>
@@ -122,6 +122,7 @@ forall (nat1:nat), add (nat1) (0) = nat1
                   | "reflexivity"
                   | "discriminate"
 
+<direction>     ::= "" | "<-"
 <target_label>  ::= <fact_label> | "goal"
 <rewrite_label> ::= <fact_label> | <lemma_label>
 <loc>           ::= "*" | "1" | "2" | ...