def Lean.Elab.Tactic.isHoleRHS (rhs : Syntax) : Bool

Equations

• Lean.Elab.Tactic.isHoleRHS rhs = (rhs.isOfKind `Lean.Parser.Term.syntheticHole || rhs.isOfKind `Lean.Parser.Term.hole)

def Lean.Elab.Tactic.evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : TacticM Unit

Equations

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

Helper method for creating an user-defined eliminator/recursor application.

structure Lean.Elab.Tactic.ElimApp.Alt : Type

• name : Name

  The short name of the alternative, used in | foo => cases

• info : Meta.ElimAltInfo
• mvarId : MVarId

  The subgoal metavariable for the alternative.

instance Lean.Elab.Tactic.ElimApp.instInhabitedAlt : Inhabited Alt

Equations

• Lean.Elab.Tactic.ElimApp.instInhabitedAlt = { default := { name := default, info := default, mvarId := default } }

structure Lean.Elab.Tactic.ElimApp.Context : Type

• elimInfo : Meta.ElimInfo
• targets : Array Expr

structure Lean.Elab.Tactic.ElimApp.State : Type

• argPos : Nat
• targetPos : Nat
• motive : Option MVarId
• f : Expr
• fType : Expr
• alts : Array Alt
• insts : Array MVarId

@[reducible, inline]

abbrev Lean.Elab.Tactic.ElimApp.M (α : Type) : Type

Equations

• Lean.Elab.Tactic.ElimApp.M = ReaderT Lean.Elab.Tactic.ElimApp.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.ElimApp.State Lean.Elab.TermElabM)

structure Lean.Elab.Tactic.ElimApp.Result : Type

• elimApp : Expr
• elimArgs : Array Expr
• motive : MVarId
• alts : Array Alt
• others : Array MVarId
• complexArgs : Array Expr

def Lean.Elab.Tactic.ElimApp.mkElimApp (elimInfo : Meta.ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result

Construct the an eliminator/recursor application. targets contains the explicit and implicit targets for the eliminator, not yet generalized. For example, the indices of builtin recursors are considered implicit targets. Remark: the method addImplicitTargets may be used to compute the sequence of implicit and explicit targets from the explicit ones.

Equations

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

partial def Lean.Elab.Tactic.ElimApp.mkElimApp.loop (elimInfo : Meta.ElimInfo) (tag : Name) : M Unit

def Lean.Elab.Tactic.ElimApp.setMotiveArg (mvarId motiveArg : MVarId) (targets : Array FVarId) (complexArgs : Array Expr := #[]) : MetaM Unit

Given a goal ... targets ... |- C[targets, complexArgs] associated with mvarId, where complexArgs are the the complex (i.e. non-target) arguments to the motive in the conclusion of the eliminator, construct motiveArg := fun targets rs => C[targets, rs]

This checks if the type of the complex arguments match what's expected by the motive, and ignores them otherwise. This limits the ability of cases to use unfolding function principles with dependent types, because after generalization of the targets, the types do no longer match. This can likely be improved.

Equations

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

def Lean.Elab.Tactic.ElimApp.evalAlts (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (initialInfo : Info) (tacStx : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit

Equations

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

def Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (tacStx : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit

Equations

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

def Lean.Elab.Tactic.ElimApp.evalAlts.goWithIncremental (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (tacStx : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) (tacSnaps : Array (Language.SnapshotBundle TacticParsedSnapshot)) : TacticM PUnit

Equations

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

def Lean.Elab.Tactic.ElimApp.evalAlts.applyAltStx (elimInfo : Meta.ElimInfo) (optPreTac : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) (tacSnaps : Array (Language.SnapshotBundle TacticParsedSnapshot)) (altStxs : Array Syntax) (altStxIdx : Nat) (altStx : Syntax) (alt : Alt) : TacticM PUnit

Applies syntactic alternative to alternative goal.

Equations

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

def Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac (optPreTac : Syntax) (mvarId : MVarId) : TacticM (List MVarId)

Applies induction .. with $preTac | .., if any, to an alternative goal.

Equations

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

def Lean.Elab.Tactic.getInductiveValFromMajor (induction : Bool) (major : Expr) : TacticM InductiveVal

Equations

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

opaque Lean.Elab.Tactic.tactic.customEliminators : Lean.Option Bool

structure Lean.Elab.Tactic.ElimTargetView : Type

View of Lean.Parser.Tactic.elimTarget.

• hIdent? : Option Ident
• term : Syntax

def Lean.Elab.Tactic.mkTargetView (target : Syntax) : TacticM ElimTargetView

Interprets a Lean.Parser.Tactic.elimTarget.

Equations

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

def Lean.Elab.Tactic.elabElimTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId))

Elaborates the targets (Lean.Parser.Tactic.elimTarget), generalizing them if requested or if otherwise necessary.

Returns

1. the targets as fvars and
2. an array of identifier/fvarid pairs so that the induction/cases tactic can annotate any user-supplied target hypothesis names using Term.addLocalVarInfo.

Modifies the current goal when generalizing.

Equations

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

def Lean.Elab.Tactic.checkInductionTargets (targets : Array Expr) : MetaM Unit

Equations

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

def Lean.Elab.Tactic.evalInduction : Tactic

Equations

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

opaque Lean.Elab.Tactic.tactic.fun_induction.unfolding : Lean.Option Bool

def Lean.Elab.Tactic.elabFunTargetCall (cases : Bool) (stx : Syntax) : TacticM Expr

Elaborates the foo args of fun_induction or fun_cases, inferring the args if omitted from the goal

Equations

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

def Lean.Elab.Tactic.evalFunInduction : Tactic

Equations

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

def Lean.Elab.Tactic.evalCasesCore (stx : Syntax) (elimInfo : Meta.ElimInfo) (targets : Array Expr) (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit

The code path shared between cases and fun_cases; when we already have an elimInfo and the targets contains the implicit targets

Equations

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

def Lean.Elab.Tactic.evalCases : Tactic

Equations

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

def Lean.Elab.Tactic.evalFunCases : Tactic

Equations

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