structure Lean.Elab.Structural.RecArgInfo : Type

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

  fixedParams : Array Lean.Expr

• recursion arguments

  ys : Array Lean.Expr

• position in ys of the argument we are recursing on

  pos : Nat

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

  indicesPos : Array Nat

• inductive datatype name of the argument we are recursing on

  indName : Lean.Name

• inductive datatype universe levels of the argument we are recursing on

  indLevels : List Lean.Level

• inductive datatype parameters of the argument we are recursing on

  indParams : Array Lean.Expr

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

  indIndices : Array Lean.Expr

• true if we are recursing over a reflexive inductive datatype

  reflexive : Bool

• true if the type is an inductive predicate

  indPred : Bool

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

• 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.

  addMatchers : Array (Lean.MetaM Unit)

@[inline]

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 : Lean.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.