Documentation

Lean.Meta.Tactic.ElimInfo

structure Lean.Meta.ElimAltInfo:

Type

name : Lean.Name
numFields : Nat

instance Lean.Meta.instReprElimAltInfo:

Repr Lean.Meta.ElimAltInfo

Equations

Lean.Meta.instReprElimAltInfo = { reprPrec := [anonymous] }

instance Lean.Meta.instInhabitedElimAltInfo:

Inhabited Lean.Meta.ElimAltInfo

Equations

Lean.Meta.instInhabitedElimAltInfo = { default := { name := default, numFields := default } }

structure Lean.Meta.ElimInfo:

Type

name : Lean.Name
motivePos : Nat
targetsPos : Array Nat
altsInfo : Array Lean.Meta.ElimAltInfo

instance Lean.Meta.instReprElimInfo:

Repr Lean.Meta.ElimInfo

Equations

Lean.Meta.instReprElimInfo = { reprPrec := [anonymous] }

instance Lean.Meta.instInhabitedElimInfo:

Inhabited Lean.Meta.ElimInfo

Equations

Lean.Meta.instInhabitedElimInfo = { default := { name := default, motivePos := default, targetsPos := default, altsInfo := default } }

def Lean.Meta.getElimInfo (declName : Lean.Name) :

Lean.MetaM Lean.Meta.ElimInfo

Equations

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

def Lean.Meta.addImplicitTargets (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) :

Lean.MetaM (Array Lean.Expr)

Eliminators/recursors may have implicit targets. For builtin recursors, all indices are implicit targets. Given an eliminator and the sequence of explicit targets, this methods returns a new sequence containing implicit and explicit targets.

Equations

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

partial def Lean.Meta.addImplicitTargets.collect (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) (type : Lean.Expr) (argIdx : Nat) (targetIdx : Nat) (targets' : Array Lean.Expr) :

Lean.MetaM (Array Lean.Expr)

structure Lean.Meta.CustomEliminator:

Type

typeNames : Array Lean.Name
elimInfo : Lean.Meta.ElimInfo

instance Lean.Meta.instInhabitedCustomEliminator:

Inhabited Lean.Meta.CustomEliminator

Equations

Lean.Meta.instInhabitedCustomEliminator = { default := { typeNames := default, elimInfo := default } }

instance Lean.Meta.instReprCustomEliminator:

Repr Lean.Meta.CustomEliminator

Equations

Lean.Meta.instReprCustomEliminator = { reprPrec := [anonymous] }

structure Lean.Meta.CustomEliminators:

Type

map : Lean.SMap (Array Lean.Name) Lean.Meta.ElimInfo

instance Lean.Meta.instInhabitedCustomEliminators:

Inhabited Lean.Meta.CustomEliminators

Equations

Lean.Meta.instInhabitedCustomEliminators = { default := { map := default } }

instance Lean.Meta.instReprCustomEliminators:

Repr Lean.Meta.CustomEliminators

Equations

Lean.Meta.instReprCustomEliminators = { reprPrec := [anonymous] }

def Lean.Meta.addCustomEliminatorEntry (es : Lean.Meta.CustomEliminators) (e : Lean.Meta.CustomEliminator) :

Lean.Meta.CustomEliminators

Equations

Lean.Meta.addCustomEliminatorEntry es e = match es with | { map := map } => { map := Lean.SMap.insert map e.typeNames e.elimInfo }

opaque Lean.Meta.customEliminatorExt:

Lean.SimpleScopedEnvExtension Lean.Meta.CustomEliminator Lean.Meta.CustomEliminators

def Lean.Meta.mkCustomEliminator (declName : Lean.Name) :

Lean.MetaM Lean.Meta.CustomEliminator

Equations

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

def Lean.Meta.addCustomEliminator (declName : Lean.Name) (attrKind : Lean.AttributeKind) :

Lean.MetaM Unit

Equations

Lean.Meta.addCustomEliminator declName attrKind = do let e ← Lean.Meta.mkCustomEliminator declName Lean.ScopedEnvExtension.add Lean.Meta.customEliminatorExt e attrKind

def Lean.Meta.getCustomEliminators:

Lean.CoreM Lean.Meta.CustomEliminators

Equations

Lean.Meta.getCustomEliminators = do let a ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.customEliminatorExt a)

def Lean.Meta.getCustomEliminator? (targets : Array Lean.Expr) :

Lean.MetaM (Option Lean.Meta.ElimInfo)

Equations

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