mkFoldlMatcher — Mathlib

Lean4
/-- Create a `Term` that represents a matcher for `foldl` notation.
Reminder: `( lit ","* => foldl (x y => scopedTerm) init)` -/
partial def mkFoldlMatcher (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 x) $(quote y) $smatcher $sinit))
Похожие утверждения