Documentation

Lean.Elab.PreDefinition.Structural.Basic

structure Lean.Elab.Structural.RecArgInfo :

Type

fixedParams : Array Lean.Expr
ys : Array Lean.Expr
pos : Nat
indicesPos : Array Nat
indName : Lean.Name
indLevels : List Lean.Level
indParams : Array Lean.Expr
indIndices : Array Lean.Expr
reflexive : Bool
indPred : Bool

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

Equations

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

structure Lean.Elab.Structural.State :

Type

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) :

Equations

Lean.Elab.Structural.recArgHasLooseBVarsAt recFnName recArgPos e = let app? := Lean.Expr.find? (fun e => Lean.Expr.isAppOf e recFnName && decide (Lean.Expr.getAppNumArgs e > recArgPos) && Lean.Expr.hasLooseBVars (Lean.Expr.getArg! e recArgPos (Lean.Expr.getAppNumArgs e))) e; Option.isSome app?

def Lean.Elab.Structural.ensureNoRecFn (recFnName : Lean.Name) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Elab.Structural.ensureNoRecFn recFnName e = if Lean.Elab.Structural.containsRecFn recFnName e = true then do Lean.Meta.forEachExpr e fun e => if Lean.Expr.isAppOf e recFnName = true then Lean.throwError (Lean.toMessageData "unexpected occurrence of recursive application" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "") else pure PUnit.unit pure e else pure e