Lean.Elab.Tactic.Induction

source

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

Bool

Equations

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

source

def Lean.Elab.Tactic.evalAlt (mvarId : Lean.MVarId) (alt : Lean.Syntax) (remainingGoals : Array Lean.MVarId) :

Lean.Elab.Tactic.TacticM (Array Lean.MVarId)

Equations

Lean.Elab.Tactic.evalAlt mvarId alt remainingGoals = let rhs := Lean.Elab.Tactic.getAltRHS alt; Lean.Elab.Tactic.withCaseRef (Lean.Elab.Tactic.getAltDArrow alt) rhs (if Lean.Elab.Tactic.isHoleRHS rhs = true then do let gs' ← Lean.Meta.withMVarContext mvarId (Lean.withRef rhs do let mvarDecl ← liftM (Lean.Meta.getMVarDecl mvarId) let val ← Lean.Elab.Tactic.elabTermEnsuringType rhs (some mvarDecl.type) false liftM (Lean.Meta.assignExprMVar mvarId val) let gs' ← liftM (Lean.Meta.getMVarsNoDelayed val) Lean.Elab.Tactic.tagUntaggedGoals mvarDecl.userName `induction (Array.toList gs') pure gs') pure (remainingGoals ++ gs') else do Lean.Elab.Tactic.setGoals [mvarId] Lean.Elab.Tactic.closeUsingOrAdmit (Lean.Elab.Tactic.withTacticInfoContext alt (Lean.Elab.Tactic.evalTactic rhs)) pure remainingGoals)

source

structure Lean.Elab.Tactic.ElimApp.Context :

Type

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

source

structure Lean.Elab.Tactic.ElimApp.State :

Type

argPos : Nat
targetPos : Nat
f : Lean.Expr
fType : Lean.Expr
alts : Array (Lean.Name × Lean.MVarId)
insts : Array Lean.MVarId

source

@[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)

source

structure Lean.Elab.Tactic.ElimApp.Result :

Type

elimApp : Lean.Expr
alts : Array (Lean.Name × Lean.MVarId)
others : Array Lean.MVarId

source

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

Lean.Elab.TermElabM Lean.Elab.Tactic.ElimApp.Result

Equations

Lean.Elab.Tactic.ElimApp.mkElimApp elimName elimInfo targets tag = (fun loop => do let f ← Lean.Elab.Term.mkConst elimName [] let fType ← liftM (Lean.Meta.inferType f) let discr ← StateRefT'.run (ReaderT.run loop { elimInfo := elimInfo, targets := targets }) { argPos := 0, targetPos := 0, f := f, fType := fType, alts := #[], insts := #[] } let x : Unit × Lean.Elab.Tactic.ElimApp.State := discr match x with | (x, s) => let others := #[]; do let r ← let col := s.insts; forIn col others fun mvarId r => let others := r; do let r ← tryCatch (do let a ← Lean.Elab.Term.synthesizeInstMVarCore mvarId none if a = true then do let y ← pure PUnit.unit pure { fst := y, snd := others } else do liftM (Lean.Meta.setMVarKind mvarId Lean.MetavarKind.syntheticOpaque) let others : Array Lean.MVarId := Array.push others mvarId let y ← pure PUnit.unit pure { fst := y, snd := others }) fun x => do liftM (Lean.Meta.setMVarKind mvarId Lean.MetavarKind.syntheticOpaque) let others : Array Lean.MVarId := Array.push others mvarId let y ← pure PUnit.unit pure { fst := y, snd := others } let x : Array Lean.MVarId := r.snd let others : Array Lean.MVarId := x pure r.fst pure (ForInStep.yield others) let x : Array Lean.MVarId := r let others : Array Lean.MVarId := x let alts ← Array.filterM (fun alt => do let a ← liftM (Lean.Meta.isExprMVarAssigned alt.snd) pure !a) s.alts 0 (Array.size s.alts) let a ← liftM (Lean.Meta.instantiateMVars s.f) pure { elimApp := a, alts := alts, others := others }) (Lean.Elab.Tactic.ElimApp.mkElimApp.loop elimName tag)

source

partial def Lean.Elab.Tactic.ElimApp.mkElimApp.loop (elimName : Lean.Name) (tag : Lean.Name) :

Lean.Elab.Tactic.ElimApp.M Unit

source

def Lean.Elab.Tactic.ElimApp.setMotiveArg (mvarId : Lean.MVarId) (motiveArg : Lean.MVarId) (targets : Array Lean.FVarId) :

Lean.MetaM Unit

Equations

Lean.Elab.Tactic.ElimApp.setMotiveArg mvarId motiveArg targets = do let type ← Lean.Meta.inferType (Lean.mkMVar mvarId) let motive ← Lean.Meta.mkLambdaFVars (Array.map Lean.mkFVar targets) type false true let motiverInferredType ← Lean.Meta.inferType motive let motiveType ← Lean.Meta.inferType (Lean.mkMVar motiveArg) let a ← Lean.Meta.isDefEqGuarded motiverInferredType motiveType let _do_jp : PUnit → Lean.MetaM Unit := fun y => Lean.Meta.assignExprMVar motiveArg motive if a = true then do let y ← pure PUnit.unit _do_jp y else do let a ← Lean.Meta.mkHasTypeButIsExpectedMsg motiverInferredType motiveType let y ← Lean.throwError (Lean.toMessageData "type mismatch when assigning motive" ++ Lean.toMessageData (Lean.indentExpr motive) ++ Lean.toMessageData "\n" ++ Lean.toMessageData a ++ Lean.toMessageData "") _do_jp y

source

def Lean.Elab.Tactic.ElimApp.evalAlts (elimInfo : Lean.Meta.ElimInfo) (alts : Array (Lean.Name × Lean.MVarId)) (optPreTac : Lean.Syntax) (altsSyntax : Array Lean.Syntax) (initialInfo : Lean.Elab.Info) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.ElimApp.evalAlts elimInfo alts optPreTac altsSyntax initialInfo numEqs numGeneralized toClear = (fun go applyPreTac => do Lean.Elab.Tactic.ElimApp.checkAltNames alts altsSyntax let hasAlts : Prop := Array.size altsSyntax > 0 if hasAlts then Lean.Elab.withInfoContext go (pure initialInfo) else go) (Lean.Elab.Tactic.ElimApp.evalAlts.go elimInfo alts optPreTac altsSyntax numEqs numGeneralized toClear) (Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac optPreTac)

source

def Lean.Elab.Tactic.ElimApp.evalAlts.go (elimInfo : Lean.Meta.ElimInfo) (alts : Array (Lean.Name × Lean.MVarId)) (optPreTac : Lean.Syntax) (altsSyntax : Array Lean.Syntax) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.ElimApp.evalAlts.go elimInfo alts optPreTac altsSyntax numEqs numGeneralized toClear = let hasAlts := Array.size altsSyntax > 0; let usedWildcard := false; let subgoals := #[]; let altsSyntax := altsSyntax; do let r ← forIn alts { fst := subgoals, snd := { fst := altsSyntax, snd := usedWildcard } } fun x r => match x with | (altName, altMVarId) => let subgoals := r.fst; let x := r.snd; let altsSyntax := x.fst; let usedWildcard := x.snd; do let numFields ← liftM (Lean.Elab.Tactic.ElimApp.getAltNumFields elimInfo altName) let isWildcard : Bool := false let _do_jp : Array Lean.MVarId → Array Lean.Syntax → Bool → Bool → Option Lean.Syntax → Lean.Elab.Tactic.TacticM (ForInStep (MProd (Array Lean.MVarId) (MProd (Array Lean.Syntax) Bool))) := fun subgoals altsSyntax isWildcard usedWildcard altStx? => match altStx? with | none => do let discr ← liftM (Lean.Meta.introN altMVarId numFields [] false) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, altMVarId) => do let a ← liftM (Lean.Meta.Cases.unifyEqs numEqs altMVarId { map := ∅ } none) match a with | none => do pure () pure (ForInStep.yield { fst := subgoals, snd := { fst := altsSyntax, snd := usedWildcard } }) | some (altMVarId', x) => do let discr ← liftM (Lean.Meta.introNP altMVarId' numGeneralized) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, altMVarId) => do let r ← forIn toClear altMVarId fun fvarId r => let altMVarId := r; do let r ← liftM (Lean.Meta.tryClear altMVarId fvarId) let altMVarId : Lean.MVarId := r pure PUnit.unit pure (ForInStep.yield altMVarId) let x : Lean.MVarId := r let altMVarId : Lean.MVarId := x let altMVarIds ← Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac optPreTac altMVarId if (!decide hasAlts) = true then let subgoals := subgoals ++ List.toArray altMVarIds; do pure PUnit.unit pure (ForInStep.yield { fst := subgoals, snd := { fst := altsSyntax, snd := usedWildcard } }) else if List.isEmpty altMVarIds = true then do pure () pure (ForInStep.yield { fst := subgoals, snd := { fst := altsSyntax, snd := usedWildcard } }) else do Lean.Elab.logError (Lean.toMessageData "alternative '" ++ Lean.toMessageData altName ++ Lean.toMessageData "' has not been provided") List.forM altMVarIds fun mvarId => liftM (Lean.Elab.admitGoal mvarId) pure (ForInStep.yield { fst := subgoals, snd := { fst := altsSyntax, snd := usedWildcard } }) | some altStx => do let discr ← Lean.withRef altStx (let unusedAlt := if isWildcard = true then pure (#[], usedWildcard) else Lean.throwError (Lean.toMessageData "alternative '" ++ Lean.toMessageData altName ++ Lean.toMessageData "' is not needed"); let altVarNames := Lean.Elab.Tactic.getAltVarNames altStx; let _do_jp := fun numFieldsToName => let cls := `Meta.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Tactic.TacticM (Array Lean.MVarId × Bool) := fun y => let _do_jp := fun y => do let discr ← liftM (Lean.Meta.introN altMVarId numFields (Array.toList altVarNames) !Lean.Elab.Tactic.altHasExplicitModifier altStx) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, altMVarId) => do let a ← liftM (Lean.Meta.Cases.unifyEqs numEqs altMVarId { map := ∅ } none) match a with | none => unusedAlt | some (altMVarId', x) => do let discr ← liftM (Lean.Meta.introNP altMVarId' numGeneralized) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, altMVarId) => do let r ← forIn toClear altMVarId fun fvarId r => let altMVarId := r; do let r ← liftM (Lean.Meta.tryClear altMVarId fvarId) let altMVarId : Lean.MVarId := r pure PUnit.unit pure (ForInStep.yield altMVarId) let x : Lean.MVarId := r let altMVarId : Lean.MVarId := x let altMVarIds ← Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac optPreTac altMVarId if List.isEmpty altMVarIds = true then unusedAlt else let subgoals := subgoals; do let r ← forIn altMVarIds subgoals fun altMVarId' r => let subgoals := r; do let r ← Lean.Elab.Tactic.evalAlt altMVarId' altStx subgoals let subgoals : Array Lean.MVarId := r pure PUnit.unit pure (ForInStep.yield subgoals) let x : Array Lean.MVarId := r let subgoals : Array Lean.MVarId := x pure (subgoals, usedWildcard || isWildcard); if Array.size altVarNames > numFieldsToName then do let y ← Lean.Elab.logError (Lean.toMessageData "too many variable names provided at alternative '" ++ Lean.toMessageData altName ++ Lean.toMessageData "', #" ++ Lean.toMessageData (Array.size altVarNames) ++ Lean.toMessageData " provided, but #" ++ Lean.toMessageData numFieldsToName ++ Lean.toMessageData " expected") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "numFields: " ++ Lean.toMessageData numFields ++ Lean.toMessageData ", numFieldsToName: " ++ Lean.toMessageData numFieldsToName ++ Lean.toMessageData ", altNames: " ++ Lean.toMessageData (Array.size altVarNames) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if Lean.Elab.Tactic.altHasExplicitModifier altStx = true then do let y ← pure numFields _do_jp y else do let y ← liftM (Lean.Elab.Tactic.ElimApp.getNumExplicitFields altMVarId numFields) _do_jp y) let x : Array Lean.MVarId × Bool := discr match x with | (subgoals, usedWildcard) => do pure PUnit.unit pure (ForInStep.yield { fst := subgoals, snd := { fst := altsSyntax, snd := usedWildcard } }) match Array.findIdx? altsSyntax fun alt => Lean.Elab.Tactic.getAltName alt == altName with | some idx => let altStx := Array.getOp altsSyntax idx; let altsSyntax := Array.eraseIdx altsSyntax idx; do let y ← pure (some altStx) _do_jp subgoals altsSyntax isWildcard usedWildcard y | none => match Array.findIdx? altsSyntax fun alt => Lean.Elab.Tactic.getAltName alt == `_ with | some idx => let isWildcard := true; do let y ← pure (some (Array.getOp altsSyntax idx)) _do_jp subgoals altsSyntax isWildcard usedWildcard y | none => do let y ← pure none _do_jp subgoals altsSyntax isWildcard usedWildcard y let x : MProd (Array Lean.MVarId) (MProd (Array Lean.Syntax) Bool) := r match x with | { fst := subgoals, snd := { fst := altsSyntax, snd := usedWildcard } } => let _do_jp := fun altsSyntax y => let _do_jp := fun y => Lean.Elab.Tactic.setGoals (Array.toList subgoals); if Array.isEmpty altsSyntax = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Elab.logErrorAt (Array.getOp altsSyntax 0) (Function.comp Lean.MessageData.ofFormat Lean.format "unused alternative") _do_jp y; if usedWildcard = true then let altsSyntax := Array.filter (fun alt => Lean.Elab.Tactic.getAltName alt != `_) altsSyntax 0 (Array.size altsSyntax); do let y ← pure PUnit.unit _do_jp altsSyntax y else do let y ← pure PUnit.unit _do_jp altsSyntax y

source

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

Lean.Elab.Tactic.TacticM (List Lean.MVarId)

Equations

Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac optPreTac mvarId = if Lean.Syntax.isNone optPreTac = true then pure [mvarId] else Lean.Elab.Tactic.evalTacticAt (Lean.Syntax.getOp optPreTac 0) mvarId

source

def Lean.Elab.Tactic.getInductiveValFromMajor (major : Lean.Expr) :

Lean.Elab.Tactic.TacticM Lean.InductiveVal

Equations

Lean.Elab.Tactic.getInductiveValFromMajor major = Lean.Elab.Tactic.liftMetaMAtMain fun mvarId => do let majorType ← Lean.Meta.inferType major let majorType ← Lean.Meta.whnf majorType Lean.matchConstInduct (Lean.Expr.getAppFn majorType) (fun x => Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "major premise type is not an inductive type " ++ Lean.toMessageData (Lean.indentExpr majorType) ++ Lean.toMessageData "") Lean.Syntax.missing) fun val x => pure val

source

def Lean.Elab.Tactic.evalInduction :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalInduction = (fun checkTargets stx => Lean.Elab.Tactic.focus do let targets ← Lean.Elab.Tactic.withMainContext (Array.mapM (fun a => Lean.Elab.Tactic.elabTerm a none false) (Lean.Syntax.getSepArgs (Lean.Syntax.getOp stx 1))) let targets ← Lean.Elab.Tactic.generalizeTargets targets let discr ← Lean.Elab.Tactic.getElimNameInfo (Lean.Syntax.getOp stx 2) targets true let x : Lean.Name × Lean.Meta.ElimInfo := discr match x with | (elimName, elimInfo) => do let mvarId ← Lean.Elab.Tactic.getMainGoal let a ← Lean.getMCtx let a_1 ← Lean.Elab.Tactic.getUnsolvedGoals let a_2 ← Lean.getRef let initInfo ← Lean.Elab.Tactic.mkTacticInfo a a_1 a_2 let tag ← liftM (Lean.Meta.getMVarTag mvarId) Lean.Meta.withMVarContext mvarId do let targets ← liftM (Lean.Meta.addImplicitTargets elimInfo targets) liftM (checkTargets targets) let targetFVarIds : Array Lean.FVarId := Array.map (fun a => Lean.Expr.fvarId! a) targets let discr ← Lean.Elab.Tactic.generalizeVars mvarId stx targets let x : Nat × Lean.MVarId := discr match x with | (n, mvarId) => Lean.Meta.withMVarContext mvarId do let result ← Lean.withRef (Lean.Syntax.getOp stx 1) (liftM (Lean.Elab.Tactic.ElimApp.mkElimApp elimName elimInfo targets tag)) let elimArgs : Array Lean.Expr := Lean.Expr.getAppArgs result.elimApp let _ ← liftM (Lean.Meta.inferType (Array.getOp elimArgs elimInfo.motivePos)) liftM (Lean.Elab.Tactic.ElimApp.setMotiveArg mvarId (Lean.Expr.mvarId! (Array.getOp elimArgs elimInfo.motivePos)) targetFVarIds) let optInductionAlts : Lean.Syntax := Lean.Syntax.getOp stx 4 let optPreTac : Lean.Syntax := Lean.Elab.Tactic.getOptPreTacOfOptInductionAlts optInductionAlts let alts : Array Lean.Syntax := Lean.Elab.Tactic.getAltsOfOptInductionAlts optInductionAlts liftM (Lean.Meta.assignExprMVar mvarId result.elimApp) Lean.Elab.Tactic.ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo 0 n targetFVarIds Lean.Elab.Tactic.appendGoals (Array.toList result.others)) Lean.Elab.Tactic.evalInduction.checkTargets

source

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

Lean.MetaM Unit

Equations

Lean.Elab.Tactic.evalInduction.checkTargets targets = let foundFVars := ∅; do let r ← forIn targets PUnit.unit fun target r => let _do_jp := fun y => if Std.RBTree.contains foundFVars (Lean.Expr.fvarId! target) = true then do Lean.throwError (Lean.toMessageData "target (or one of its indices) occurs more than once" ++ Lean.toMessageData (Lean.indentExpr target) ++ Lean.toMessageData "") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit); if Lean.Expr.isFVar target = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "index in target's type is not a variable (consider using the `cases` tactic instead)" ++ Lean.toMessageData (Lean.indentExpr target) ++ Lean.toMessageData "") _do_jp y let x : PUnit := r pure PUnit.unit

source

def Lean.Elab.Tactic.elabCasesTargets (targets : Array Lean.Syntax) :

Lean.Elab.Tactic.TacticM (Array Lean.Expr)

Equations

Lean.Elab.Tactic.elabCasesTargets targets = Lean.Elab.Tactic.withMainContext do let args ← Array.mapM (fun target => let hName? := if Lean.Syntax.isNone (Lean.Syntax.getOp target 0) = true then none else some (Lean.Syntax.getId (Lean.Syntax.getOp (Lean.Syntax.getOp target 0) 0)); do let expr ← Lean.Elab.Tactic.elabTerm (Lean.Syntax.getOp target 1) none false pure { expr := expr, xName? := none, hName? := hName? }) targets if Array.all args (fun arg => Lean.Expr.isFVar arg.expr && Option.isNone arg.hName?) 0 (Array.size args) = true then pure (Array.map (fun a => a.expr) args) else Lean.Elab.Tactic.liftMetaTacticAux fun mvarId => do let argsToGeneralize ← pure (Array.filter (fun arg => !(Lean.Expr.isFVar arg.expr && Option.isNone arg.hName?)) args 0 (Array.size args)) let discr ← Lean.Meta.generalize mvarId argsToGeneralize let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (fvarIdsNew, mvarId) => let result := #[]; let j := 0; do let r ← forIn args { fst := j, snd := result } fun arg r => let j := r.fst; let result := r.snd; if (Lean.Expr.isFVar arg.expr && Option.isNone arg.hName?) = true then let result := Array.push result arg.expr; do pure PUnit.unit pure (ForInStep.yield { fst := j, snd := result }) else let result := Array.push result (Lean.mkFVar (Array.getOp fvarIdsNew j)); let j := j + 1; do pure PUnit.unit pure (ForInStep.yield { fst := j, snd := result }) let x : MProd Nat (Array Lean.Expr) := r match x with | { fst := j, snd := result } => pure (result, [mvarId])

source

def Lean.Elab.Tactic.evalCases :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalCases stx = Lean.Elab.Tactic.focus do let targets ← Lean.Elab.Tactic.elabCasesTargets (Lean.Syntax.getSepArgs (Lean.Syntax.getOp stx 1)) let optInductionAlts : Lean.Syntax := Lean.Syntax.getOp stx 3 let optPreTac : Lean.Syntax := Lean.Elab.Tactic.getOptPreTacOfOptInductionAlts optInductionAlts let alts : Array Lean.Syntax := Lean.Elab.Tactic.getAltsOfOptInductionAlts optInductionAlts let targetRef : Lean.Syntax := Lean.Syntax.getOp stx 1 let discr ← Lean.Elab.Tactic.getElimNameInfo (Lean.Syntax.getOp stx 2) targets false let x : Lean.Name × Lean.Meta.ElimInfo := discr match x with | (elimName, elimInfo) => do let mvarId ← Lean.Elab.Tactic.getMainGoal let a ← Lean.getMCtx let a_1 ← Lean.Elab.Tactic.getUnsolvedGoals let a_2 ← Lean.getRef let initInfo ← Lean.Elab.Tactic.mkTacticInfo a a_1 a_2 let tag ← liftM (Lean.Meta.getMVarTag mvarId) Lean.Meta.withMVarContext mvarId do let targets ← liftM (Lean.Meta.addImplicitTargets elimInfo targets) let result ← Lean.withRef targetRef (liftM (Lean.Elab.Tactic.ElimApp.mkElimApp elimName elimInfo targets tag)) let elimArgs : Array Lean.Expr := Lean.Expr.getAppArgs result.elimApp let targets ← Array.mapM (fun i => liftM (Lean.Meta.instantiateMVars (Array.getOp elimArgs i))) elimInfo.targetsPos let motiveType ← liftM (Lean.Meta.inferType (Array.getOp elimArgs elimInfo.motivePos)) let mvarId ← liftM (Lean.Meta.generalizeTargetsEq mvarId motiveType targets) let discr ← liftM (Lean.Meta.introN mvarId (Array.size targets) [] false) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (targetsNew, mvarId) => Lean.Meta.withMVarContext mvarId do liftM (Lean.Elab.Tactic.ElimApp.setMotiveArg mvarId (Lean.Expr.mvarId! (Array.getOp elimArgs elimInfo.motivePos)) targetsNew) liftM (Lean.Meta.assignExprMVar mvarId result.elimApp) Lean.Elab.Tactic.ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (Array.size targets) 0 targetsNew