Equations
- Lean.Elab.Structural.RecArgInfo.recArgPos info = Array.size info.fixedParams + info.pos
@[inline]
Equations
- Lean.Elab.Structural.instInhabitedM = { default := Lean.throwError (Lean.toMessageData "failed") }
def
Lean.Elab.Structural.run
{α : Type}
(x : Lean.Elab.Structural.M α)
(s : optParam Lean.Elab.Structural.State { addMatchers := #[] })
:
Equations
- Lean.Elab.Structural.run x s = StateRefT'.run x s
def
Lean.Elab.Structural.recArgHasLooseBVarsAt
(recFnName : Lean.Name)
(recArgPos : Nat)
(e : Lean.Expr)
:
Return true iff e contains an application recFnName .. t .. where the term t is
the argument we are trying to recurse on, and it contains loose bound variables.
We use this test to decide whether we should process a matcher-application as a regular
applicaton or not. That is, whether we should push the below argument should be affected by the matcher or not.
If e does not contain an application of the form recFnName .. t .., then we know
the recursion doesn't depend on any pattern variable in this matcher.
Equations
- One or more equations did not get rendered due to their size.