Lean4
/-- `congr(expr)` generates a congruence from an expression containing
congruence holes of the form `$h` or `$(h)`.
In these congruence holes, `h : a = b` indicates that, in the generated congruence,
on the left-hand side `a` is substituted for `$h`
and on the right-hand side `b` is substituted for `$h`.
For example, if `h : a = b` then `congr(1 + $h) : 1 + a = 1 + b`.
This is able to make use of the expected type, for example `(congr(_ + $h) : 1 + _ = _)`
with `h : x = y` gives `1 + x = 1 + y`.
The expected type can be an `Iff`, `Eq`, or `HEq`.
If there is no expected type, then it generates an equality.
Note: the process of generating a congruence lemma involves elaborating the pattern
using terms with attached metadata and a reducible wrapper.
We try to avoid doing so, but these terms can leak into the local context through unification.
This can potentially break tactics that are sensitive to metadata or reducible functions.
Please report anything that goes wrong with `congr(...)` lemmas on Zulip.
For debugging, you can set `set_option trace.Elab.congr true`.
-/
@[term_parser 1000]
public meta def termCongr : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.TermCongr.termCongr 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "congr(")
(ParserDescr.unary✝ `withoutForbidden (ParserDescr.unary✝ `ppDedentIfGrouped (ParserDescr.cat✝ `term 0))))
(ParserDescr.symbol✝ ")"))
