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.

@[reducible, 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 : 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 application 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.

@[reducible, inline]

abbrev Lean.Elab.Structural.Positions : Type

Lets say we have n mutually recursive functions whose recursive arguments are from a group of m mutually inductive data types. This mapping does not have to be one-to-one: for one type there can be zero, one or more functions. We use the logic in the FunPacker modules to combine the bodies (and motives) of multiple such functions.

Therefore we have to take the n functions, group them by their recursive argument's type, and for each such type, keep track of the order of the functions.

We represent these positions as an Array (Array Nat). We have that

• positions.size = indInfo.numTypeFormers
• positions.flatten is a permutation of [0:n], so each of the n functions has exactly one position, and each position refers to one of the n functions.
• if k ∈ positions[i] then the recursive argument of function k is has type indInfo.all[i] (or corresponding nested inductive type)

Equations

• Lean.Elab.Structural.Positions = Array (Array Nat)

def Lean.Elab.Structural.Positions.numIndices (positions : Lean.Elab.Structural.Positions) : Nat

The number of indices in the array.

Equations

• positions.numIndices = Array.foldl (fun (s : Nat) (poss : Array Nat) => s + poss.size) 0 positions

def Lean.Elab.Structural.Positions.groupAndSort {α : Type u_1} {β : Type u_2} [Inhabited α] [DecidableEq β] (f : α → β) (xs : Array α) (ys : Array β) : Lean.Elab.Structural.Positions

Groups the xs by their f value, and puts these groups into the order given by ys.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Structural.Positions.mapMwith {γ : Type u_1} {α : Type u_2} {β : Type u_3} {m : Type u_1 → Type u_4} [Monad m] [Inhabited β] (f : α → Array β → m γ) (positions : Lean.Elab.Structural.Positions) (ys : Array α) (xs : Array β) : m (Array γ)

Let positions.size = ys.size and positions.numIndices = xs.size. Maps f over each y in ys, also passing in those elements xs that belong to that are those elements of xs that belong to y according to positions.

Equations

• One or more equations did not get rendered due to their size.