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
• motive : MVarId
• alts : Array Alt
• others : Array MVarId

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. 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) : MetaM Unit

Given a goal ... targets ... |- C[targets] associated with mvarId, assign motiveArg := fun targets => C[targets]

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) (numEqs numGeneralized : Nat := 0) (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)) (numEqs numGeneralized : Nat := 0) (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)) (numEqs numGeneralized : Nat := 0) (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 numGeneralized : Nat := 0) (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.

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.