mkFoldrMatcher — Mathlib

Lean4
/-- Create a `Term` that represents a matcher for `foldr` notation.
Reminder: `( lit ","* => foldr (x y => scopedTerm) init)` -/
partial def mkFoldrMatcher (lit x y : Name) (scopedTerm init : Term) (boundNames : Array Name) :
    OptionT TermElabM (List DelabKey × Term) := do
  -- Build the `scopedTerm` matcher with `x` and `y` as additional variables

  let boundNames' := boundNames |>.push x |>.push y
  let (keys, smatcher) ← mkExprMatcher scopedTerm boundNames'
  let (keys', sinit) ← mkExprMatcher init boundNames
  return (keys ++ keys', ← ``(matchFoldl $(quote lit) $(quote y) $(quote x) $smatcher $sinit))
Похожие утверждения