structure Lean.Elab.Structural.RecArgInfo : Type

• fixedParams : Array Lean.Expr

  fixedParams ++ ys are the arguments of the function we are trying to justify termination using structural recursion.

• ys : Array Lean.Expr

  recursion arguments

• pos : Nat

  position in ys of the argument we are recursing on

• indicesPos : Array Nat

  position in ys of the inductive datatype indices we are recursing on

• indName : Lake.Name

  inductive datatype name of the argument we are recursing on

• indLevels : List Lean.Level

  inductive datatype universe levels of the argument we are recursing on

• indParams : Array Lean.Expr

  inductive datatype parameters of the argument we are recursing on

• indIndices : Array Lean.Expr

  inductive datatype indices of the argument we are recursing on, it is equal to indicesPos.map fun i => ys.get! i

• reflexive : Bool

  true if we are recursing over a reflexive inductive datatype

• indPred : Bool

  true if the type is an inductive predicate

def Lean.Elab.Structural.RecArgInfo.recArgPos (info : Lean.Elab.Structural.RecArgInfo) : Nat

Equations

• Lean.Elab.Structural.RecArgInfo.recArgPos info = Array.size info.fixedParams + info.pos

structure Lean.Elab.Structural.State : Type

• addMatchers : Array (Lean.MetaM Unit)

  As part of the inductive predicates case, we keep adding more and more discriminants from the local context and build up a bigger matcher application until we reach a fixed point. As a side-effect, this creates matchers. Here we capture all these side-effects, because the construction rolls back any changes done to the environment and the side-effects need to be replayed.

@[inline, reducible]

abbrev Lean.Elab.Structural.M (α : Type) : Type

Equations

• Lean.Elab.Structural.M = StateRefT' IO.RealWorld Lean.Elab.Structural.State Lean.MetaM

instance Lean.Elab.Structural.instInhabitedM {α : Type} : Inhabited (Lean.Elab.Structural.M α)

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 := #[] }) : Lean.MetaM (α × Lean.Elab.Structural.State)

Equations

• Lean.Elab.Structural.run x s = StateRefT'.run x s

def Lean.Elab.Structural.recArgHasLooseBVarsAt (recFnName : Lake.Name) (recArgPos : Nat) (e : Lean.Expr) : Bool

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.