Lean4
/-- Returns a `Term` that represents a `Matcher` for the given pattern `stx`.
The `boundNames` set determines which identifiers are variables in the pattern.
Fails in the `OptionT` sense if it comes across something it's unable to handle.
Also returns constant names that could serve as a key for a delaborator.
For example, if it's for a function `f`, then `app.f`. -/
partial def mkExprMatcher (stx : Term) (boundNames : Array Name) : OptionT TermElabM (List DelabKey × Term) := do
let (lctx, boundFVars) ← setupLCtx (← getLCtx) boundNames
withLCtx lctx (← getLocalInstances)
(do
let patt ←
try
Term.elabPattern stx none
catch e =>
logException e
trace[notation3]"Could not elaborate pattern{(indentD stx)}\nError: {e.toMessageData}"
failure
trace[notation3]"Generating matcher for pattern {patt}"
exprToMatcher boundFVars { } patt)
