Skip to content

Commit 23d76ae

Browse files
committed
chore(Mathport/Syntax): add syntax for coherence tactic (#310)
Should have been added after leanprover-community/mathlib3#13417. Co-authored-by: Scott Morrison <[email protected]>
1 parent d82ec3a commit 23d76ae

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

Mathlib/Mathport/Syntax.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -523,6 +523,9 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
523523
/- E -/ syntax (name := ghostSimp) "ghost_simp" (" [" simpArg,* "]")? : tactic
524524
/- E -/ syntax (name := wittTruncateFunTac) "witt_truncate_fun_tac" : tactic
525525

526+
/- M -/ @[nolint docBlame] syntax (name := pure_coherence) "pure_coherence" : tactic
527+
/- M -/ @[nolint docBlame] syntax (name := coherence) "coherence" : tactic
528+
526529
namespace Conv
527530

528531
-- https://github.com/leanprover-community/mathlib/issues/2882

0 commit comments

Comments
 (0)