Skip to content

Commit cffa617

Browse files
authored
fix: incorrect arrow orientations in grind syntax
1 parent bd14e70 commit cffa617

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Init/Grind/Tactics.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ syntax grindEq := "= "
1919
syntax grindEqBoth := atomic("_" "=" "_ ")
2020
syntax grindEqRhs := atomic("=" "_ ")
2121
syntax grindEqBwd := atomic("←" "= ") <|> atomic("<-" "= ")
22-
syntax grindBwd := "← " <|> "-> "
23-
syntax grindFwd := "→ " <|> "<- "
22+
syntax grindBwd := "← " <|> "<- "
23+
syntax grindFwd := "→ " <|> "-> "
2424
syntax grindRL := "⇐ " <|> "<= "
2525
syntax grindLR := "⇒ " <|> "=> "
2626
syntax grindUsr := &"usr "

0 commit comments

Comments
 (0)