Lean4
/-- (Internal for `congr(...)`)
Elaborates to an expression satisfying `cHole?` that equals the LHS or RHS of `h`,
if the LHS or RHS is available after elaborating `h`. Uses the expected type as a hint. -/
@[term_parser 1000]
public meta def cHoleExpand : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.TermCongr.cHoleExpand 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "cHole% ")
(ParserDescr.binary✝ `orelse
(ParserDescr.nodeWithAntiquot✝ "lhs" `token.lhs
((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "lhs" false✝))
(ParserDescr.nodeWithAntiquot✝ "rhs" `token.rhs
((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "rhs" false✝))))
(ParserDescr.cat✝ `term 0))
