def Lean.Elab.Tactic.isHoleRHS (rhs : Lean.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 : Lean.MVarId) (alt : Lean.Syntax) (addInfo : Lean.Elab.TermElabM Unit) : Lean.Elab.Tactic.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 : Lean.Name

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

• info : Lean.Meta.ElimAltInfo
• mvarId : Lean.MVarId

  The subgoal metavariable for the alternative.

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

Equations

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

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

• elimInfo : Lean.Meta.ElimInfo
• targets : Array Lean.Expr

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

• argPos : Nat
• targetPos : Nat
• motive : Option Lean.MVarId
• f : Lean.Expr
• fType : Lean.Expr
• alts : Array Lean.Elab.Tactic.ElimApp.Alt
• insts : Array Lean.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 : Lean.Expr
• motive : Lean.MVarId
• alts : Array Lean.Elab.Tactic.ElimApp.Alt
• others : Array Lean.MVarId

def Lean.Elab.Tactic.ElimApp.mkElimApp (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) (tag : Lean.Name) : Lean.Elab.TermElabM Lean.Elab.Tactic.ElimApp.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 : Lean.Meta.ElimInfo) (tag : Lean.Name) : Lean.Elab.Tactic.ElimApp.M Unit

def Lean.Elab.Tactic.ElimApp.setMotiveArg (mvarId : Lean.MVarId) (motiveArg : Lean.MVarId) (targets : Array Lean.FVarId) : Lean.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 : Lean.Meta.ElimInfo) (alts : Array Lean.Elab.Tactic.ElimApp.Alt) (optPreTac : Lean.Syntax) (altStxs : Array Lean.Syntax) (initialInfo : Lean.Elab.Info) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) (toTag : optParam (Array (Lean.Ident × Lean.FVarId)) #[]) : Lean.Elab.Tactic.TacticM Unit

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.ElimApp.evalAlts.applyAltStx (elimInfo : Lean.Meta.ElimInfo) (optPreTac : Lean.Syntax) (altStxs : Array Lean.Syntax) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) (toTag : optParam (Array (Lean.Ident × Lean.FVarId)) #[]) (tacSnaps : Array (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)) (altStxIdx : Nat) (altStx : Lean.Syntax) (alt : Lean.Elab.Tactic.ElimApp.Alt) : Lean.Elab.Tactic.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 : Lean.Syntax) (mvarId : Lean.MVarId) : Lean.Elab.Tactic.TacticM (List Lean.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 (major : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.InductiveVal

Equations

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

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

def Lean.Elab.Tactic.evalInduction : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.evalCases : Lean.Elab.Tactic.Tactic

Equations

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