mkScopedMatcher — Mathlib

Lean4
/-- Create a `Term` that represents a matcher for `scoped` notation.
Fails in the `OptionT` sense if a matcher couldn't be constructed.
Also returns a delaborator key like in `mkExprMatcher`.
Reminder: `$lit:ident : (scoped $scopedId:ident => $scopedTerm:Term)` -/
partial def mkScopedMatcher (lit scopeId : Name) (scopedTerm : Term) (boundNames : Array Name) :
    OptionT TermElabM (List DelabKey × Term) := do
  -- Build the matcher for `scopedTerm` with `scopeId` as an additional variable

  let (keys, smatcher) ← mkExprMatcher scopedTerm (boundNames.push scopeId)
  return (keys, ← ``(matchScoped $(quote lit) $(quote scopeId) $smatcher))
Похожие утверждения