Lean.Elab.Tactic.BuiltinTactic

Lean.Elab.Tactic.evalOpen stx = tryFinally (do Lean.pushScope let openDecls ← Lean.Elab.elabOpenDecl (Lean.Syntax.getOp stx 1) withTheReader Lean.Core.Context (fun ctx => { options := ctx.options, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) (Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 3))) Lean.popScope

source

def Lean.Elab.Tactic.elabSetOption :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.elabSetOption stx = do let options ← Lean.Elab.elabSetOption (Lean.Syntax.getOp stx 1) (Lean.Syntax.getOp stx 2) withTheReader Lean.Core.Context (fun ctx => { options := options, currRecDepth := ctx.currRecDepth, maxRecDepth := Lean.Option.get options Lean.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) (Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 4))

source

def Lean.Elab.Tactic.evalAllGoals :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalAllGoals stx = do let mvarIds ← Lean.Elab.Tactic.getGoals let mvarIdsNew : Array Lean.MVarId := #[] let r ← forIn mvarIds mvarIdsNew fun mvarId r => let mvarIdsNew := r; do let a ← liftM (Lean.Meta.isExprMVarAssigned mvarId) if a = true then do pure PUnit.unit pure (ForInStep.yield mvarIdsNew) else do Lean.Elab.Tactic.setGoals [mvarId] let r ← tryCatch (do Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 1) let a ← Lean.Elab.Tactic.getUnsolvedGoals let mvarIdsNew : Array Lean.MVarId := mvarIdsNew ++ a let y ← pure PUnit.unit pure { fst := y, snd := mvarIdsNew }) fun ex => do Lean.Elab.logException ex let mvarIdsNew : Array Lean.MVarId := Array.push mvarIdsNew mvarId let y ← pure PUnit.unit pure { fst := y, snd := mvarIdsNew } let x : Array Lean.MVarId := r.snd let mvarIdsNew : Array Lean.MVarId := x pure r.fst pure (ForInStep.yield mvarIdsNew) let x : Array Lean.MVarId := r let mvarIdsNew : Array Lean.MVarId := x Lean.Elab.Tactic.setGoals (Array.toList mvarIdsNew)

source

def Lean.Elab.Tactic.evalAnyGoals :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalAnyGoals stx = do let mvarIds ← Lean.Elab.Tactic.getGoals let mvarIdsNew : Array Lean.MVarId := #[] let succeeded : Bool := false let r ← forIn mvarIds { fst := succeeded, snd := mvarIdsNew } fun mvarId r => let succeeded := r.fst; let mvarIdsNew := r.snd; do let a ← liftM (Lean.Meta.isExprMVarAssigned mvarId) if a = true then do pure PUnit.unit pure (ForInStep.yield { fst := succeeded, snd := mvarIdsNew }) else do Lean.Elab.Tactic.setGoals [mvarId] let r ← tryCatch (do Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 1) let a ← Lean.Elab.Tactic.getUnsolvedGoals let mvarIdsNew : Array Lean.MVarId := mvarIdsNew ++ a let succeeded : Bool := true let y ← pure PUnit.unit pure { fst := y, snd := { fst := succeeded, snd := mvarIdsNew } }) fun x => let mvarIdsNew := Array.push mvarIdsNew mvarId; do let y ← pure PUnit.unit pure { fst := y, snd := { fst := succeeded, snd := mvarIdsNew } } let x : MProd Bool (Array Lean.MVarId) := r.snd match x with | { fst := succeeded, snd := mvarIdsNew } => do pure r.fst pure (ForInStep.yield { fst := succeeded, snd := mvarIdsNew }) let x : MProd Bool (Array Lean.MVarId) := r match x with | { fst := succeeded, snd := mvarIdsNew } => let _do_jp := fun y => Lean.Elab.Tactic.setGoals (Array.toList mvarIdsNew); if succeeded = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "failed on all goals") _do_jp y

source

def Lean.Elab.Tactic.evalTacticSeq :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalTacticSeq stx = Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 0)

source

partial def Lean.Elab.Tactic.evalChoiceAux (tactics : Array Lean.Syntax) (i : Nat) :

Lean.Elab.Tactic.TacticM Unit

source

def Lean.Elab.Tactic.evalChoice :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalChoice stx = Lean.Elab.Tactic.evalChoiceAux (Lean.Syntax.getArgs stx) 0

source

def Lean.Elab.Tactic.evalSkip :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalSkip stx = pure ()

source

def Lean.Elab.Tactic.evalUnknown :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalUnknown stx = do let a ← Lean.Elab.Tactic.getGoals Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.tactic stx a)

source

def Lean.Elab.Tactic.evalFailIfSuccess :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalFailIfSuccess stx = let tactic := Lean.Syntax.getOp stx 1; do let a ← tryCatch (do Lean.Elab.Tactic.evalTactic tactic pure true) fun x => pure false if a = true then Lean.throwError (Lean.toMessageData "tactic succeeded") else pure PUnit.unit

source

def Lean.Elab.Tactic.evalTraceState :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalTraceState stx = do let gs ← Lean.Elab.Tactic.getUnsolvedGoals Lean.Elab.logInfo (Lean.Elab.goalsToMessageData gs)

source

def Lean.Elab.Tactic.evalAssumption :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalAssumption stx = Lean.Elab.Tactic.liftMetaTactic fun mvarId => do Lean.Meta.assumption mvarId pure []

source

def Lean.Elab.Tactic.evalContradiction :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalContradiction stx = Lean.Elab.Tactic.liftMetaTactic fun mvarId => do Lean.Meta.contradiction mvarId { useDecide := true, searchFuel := 16, genDiseq := false } pure []

source

def Lean.Elab.Tactic.evalIntro :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalIntro = (fun introStep stx => let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.intro = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 0 = true then introStep `_ else let discr_3 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_3 1 = true then let discr := Lean.Syntax.getArg discr_3 0; cond (Lean.Syntax.isOfKind discr `ident) (let h := discr; introStep (Lean.Syntax.getId h)) (let discr := Lean.Syntax.getArg discr_3 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.hole = true then let discr := Lean.Syntax.getArg discr 0; introStep `_ else let discr := Lean.Syntax.getArg discr_3 0; let pat := discr; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.seq1 #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.intro #[Lean.Syntax.atom info "intro", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []]], Lean.Syntax.atom info ";", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[pat], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.syntheticHole #[Lean.Syntax.atom info "?", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]]]]]], Lean.Syntax.atom info ";", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticTry_ #[Lean.Syntax.atom info "try", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.clear #[Lean.Syntax.atom info "clear", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]]) Lean.Elab.Tactic.evalTactic a) else let discr_4 := Lean.Syntax.getArg discr 1; if Lean.Syntax.getNumArgs discr_4 ≥ 1 then let discr := Lean.Syntax.getArg discr_4 0; let discr_5 := Lean.mkNullNode (Array.extract (Lean.Syntax.getArgs discr_4) 1 (Lean.Syntax.getNumArgs discr_4 - 0)); let hs := Lean.Syntax.getArgs discr_5; let h := discr; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.seq1 #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.intro #[Lean.Syntax.atom info "intro", Lean.Syntax.node Lean.SourceInfo.none `null #[h]], Lean.Syntax.atom info ";", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.intro #[Lean.Syntax.atom info "intro", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] hs)]]]) Lean.Elab.Tactic.evalTactic a else let discr := Lean.Syntax.getArg discr 1; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax) Lean.Elab.Tactic.evalIntro.introStep

source

def Lean.Elab.Tactic.evalIntro.introStep (n : Lean.Name) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.evalIntro.introStep n = Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let discr ← Lean.Meta.intro mvarId n let x : Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => pure [mvarId]

source

def Lean.Elab.Tactic.evalIntroMatch :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalIntroMatch stx = let matchAlts := Lean.Syntax.getOp stx 1; do let stxNew ← Lean.Elab.liftMacroM (Lean.Elab.Term.expandMatchAltsIntoMatchTactic stx matchAlts) Lean.Elab.Tactic.withMacroExpansion stx stxNew (Lean.Elab.Tactic.evalTactic stxNew)

source

def Lean.Elab.Tactic.evalIntros :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalIntros stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.intros = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 0 = true then Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let discr ← Lean.Meta.intros mvarId let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => pure [mvarId] else let discr := Lean.Syntax.getArg discr 1; let ids := Lean.Syntax.getArgs discr; Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let discr ← Lean.Meta.introN mvarId (Array.size ids) (Array.toList (Array.map Lean.Elab.Tactic.getNameOfIdent' ids)) false let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => pure [mvarId] else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalRevert :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalRevert stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.revert = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let hs := Lean.Syntax.getArgs discr; do let a ← Lean.Elab.Tactic.getMainGoal let a_1 ← Lean.Elab.Tactic.getFVarIds hs let discr ← liftM (Lean.Meta.revert a a_1 false) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => Lean.Elab.Tactic.replaceMainGoal [mvarId] else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalClear :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalClear stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.clear = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let hs := Lean.Syntax.getArgs discr; do let fvarIds ← Lean.Elab.Tactic.getFVarIds hs let fvarIds ← Lean.Elab.Tactic.withMainContext (liftM (Lean.Meta.sortFVarIds fvarIds)) let r ← let col := Array.reverse fvarIds; forIn col PUnit.unit fun fvarId r => do Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainGoal let mvarId ← liftM (Lean.Meta.clear a fvarId) Lean.Elab.Tactic.replaceMainGoal [mvarId] pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.forEachVar (hs : Array Lean.Syntax) (tac : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.forEachVar hs tac = do let r ← forIn hs PUnit.unit fun h r => do Lean.Elab.Tactic.withMainContext do let fvarId ← Lean.Elab.Tactic.getFVarId h let a ← Lean.Elab.Tactic.getMainGoal let mvarId ← liftM (tac a fvarId) Lean.Elab.Tactic.replaceMainGoal [mvarId] pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

def Lean.Elab.Tactic.evalSubst :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalSubst stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.subst = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let hs := Lean.Syntax.getArgs discr; Lean.Elab.Tactic.forEachVar hs Lean.Meta.subst else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.renameInaccessibles (mvarId : Lean.MVarId) (hs : Array Lean.Syntax) :

Lean.Elab.Tactic.TacticM Lean.MVarId

Equations

Lean.Elab.Tactic.renameInaccessibles mvarId hs = if Array.isEmpty hs = true then pure mvarId else do let mvarDecl ← liftM (Lean.Meta.getMVarDecl mvarId) let lctx : Lean.LocalContext := mvarDecl.lctx let hs : Array Lean.Syntax := hs let found : Lean.NameSet := ∅ let n : Nat := Lean.LocalContext.numIndices lctx let r ← let col := { start := 0, stop := n, step := 1 }; forIn col { fst := found, snd := { fst := lctx, snd := hs } } fun i r => let found := r.fst; let x := r.snd; let lctx := x.fst; let hs := x.snd; let j := n - i - 1; match Lean.LocalContext.getAt? lctx j with | none => do pure () pure (ForInStep.yield { fst := found, snd := { fst := lctx, snd := hs } }) | some localDecl => let _do_jp := fun found lctx hs y => let found := Lean.NameSet.insert found (Lean.LocalDecl.userName localDecl); do pure PUnit.unit pure (ForInStep.yield { fst := found, snd := { fst := lctx, snd := hs } }); if (Lean.Name.hasMacroScopes (Lean.LocalDecl.userName localDecl) || Lean.NameSet.contains found (Lean.LocalDecl.userName localDecl)) = true then let h := Array.back hs; let _do_jp := fun lctx hs y => let hs := Array.pop hs; if Array.isEmpty hs = true then pure (ForInStep.done { fst := found, snd := { fst := lctx, snd := hs } }) else do let y ← pure PUnit.unit _do_jp found lctx hs y; if Lean.Syntax.isIdent h = true then let newName := Lean.Syntax.getId h; let lctx := Lean.LocalContext.setUserName lctx (Lean.LocalDecl.fvarId localDecl) newName; do let y ← pure PUnit.unit _do_jp lctx hs y else do let y ← pure PUnit.unit _do_jp lctx hs y else do let y ← pure PUnit.unit _do_jp found lctx hs y let x : MProd Lean.NameSet (MProd Lean.LocalContext (Array Lean.Syntax)) := r match x with | { fst := found, snd := { fst := lctx, snd := hs } } => let _do_jp := fun y => do let mvarNew ← liftM (Lean.Meta.mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type Lean.MetavarKind.syntheticOpaque mvarDecl.userName 0) liftM (Lean.Meta.assignExprMVar mvarId mvarNew) pure (Lean.Expr.mvarId! mvarNew); if Array.isEmpty hs = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Elab.logError (Lean.toMessageData "too many variable names provided") _do_jp y

source

def Lean.Elab.Tactic.evalCase :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalCase x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.case = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr_4 := Lean.Syntax.getArg discr 3; let discr_5 := Lean.Syntax.getArg discr 4; cond (Lean.Syntax.isOfKind discr_5 `Lean.Parser.Tactic.tacticSeq) (let tac := discr_5; let arr := discr_4; let hs := Lean.Syntax.getArgs discr_3; let tag := discr_2; let stx := discr; do let gs ← Lean.Elab.Tactic.getUnsolvedGoals let _do_jp : Lean.MVarId → Lean.Elab.Tactic.TacticM Unit := fun g => let gs := List.erase gs g; do let g ← Lean.Elab.Tactic.renameInaccessibles g hs Lean.Elab.Tactic.setGoals [g] let savedTag ← liftM (Lean.Meta.getMVarTag g) liftM (Lean.Meta.setMVarTag g Lean.Name.anonymous) tryFinally (Lean.Elab.Tactic.withCaseRef arr tac (Lean.Elab.Tactic.closeUsingOrAdmit (Lean.Elab.Tactic.withTacticInfoContext stx (Lean.Elab.Tactic.evalTactic tac)))) (liftM (Lean.Meta.setMVarTag g savedTag)) Lean.Elab.Tactic.done Lean.Elab.Tactic.setGoals gs if Lean.Syntax.isIdent tag = true then let tag := Lean.Syntax.getId tag; do let discr ← Lean.Elab.Tactic.findTag? gs tag match discr with | some g => do let y ← pure g _do_jp y | x => do let y ← Lean.throwError (Lean.toMessageData "tag not found") _do_jp y else do let y ← Lean.Elab.Tactic.getMainGoal _do_jp y) (let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax) else let discr := x; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalRenameInaccessibles :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalRenameInaccessibles x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.renameI = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let hs := Lean.Syntax.getArgs discr_2; let stx := discr; do let a ← Lean.Elab.Tactic.getMainGoal let a ← Lean.Elab.Tactic.renameInaccessibles a hs Lean.Elab.Tactic.replaceMainGoal [a] else let discr := x; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalFirst :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalFirst = (fun loop stx => let tacs := Lean.Syntax.getArgs (Lean.Syntax.getOp stx 1); let _do_jp := fun y => loop tacs 0; if Array.isEmpty tacs = true then do let y ← Lean.Elab.throwUnsupportedSyntax _do_jp y else do let y ← pure PUnit.unit _do_jp y) Lean.Elab.Tactic.evalFirst.loop

source

partial def Lean.Elab.Tactic.evalFirst.loop (tacs : Array Lean.Syntax) (i : Nat) :

Lean.Elab.Tactic.TacticM Unit