Lean.Elab.Tactic.Basic

Lean.Elab.Tactic.run mvarId x = Lean.Meta.withMVarContext mvarId do let a ← get let savedSyntheticMVars : List Lean.Elab.Term.SyntheticMVarDecl := a.syntheticMVars modify fun s => { levelNames := s.levelNames, syntheticMVars := [], mvarErrorInfos := s.mvarErrorInfos, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState } let aux : Lean.Elab.Tactic.TacticM (List Lean.MVarId) := tryCatch (do x Lean.Elab.Tactic.getUnsolvedGoals) fun ex => if Lean.Elab.isAbortTacticException ex = true then Lean.Elab.Tactic.getUnsolvedGoals else throw ex tryFinally (Lean.Elab.Tactic.TacticM.runCore' aux { main := mvarId, elaborator := Lean.Name.anonymous } { goals := [mvarId] }) (modify fun s => { levelNames := s.levelNames, syntheticMVars := savedSyntheticMVars, mvarErrorInfos := s.mvarErrorInfos, messages := s.messages, letRecsToLift := s.letRecsToLift, infoState := s.infoState })

source

def Lean.Elab.Tactic.saveState :

Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.SavedState

Equations

Lean.Elab.Tactic.saveState = do let a ← liftM Lean.Elab.Term.saveState let a_1 ← get pure { term := a, tactic := a_1 }

source

def Lean.Elab.Tactic.SavedState.restore (b : Lean.Elab.Tactic.SavedState) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.SavedState.restore b = do liftM (Lean.Elab.Term.SavedState.restore b.term false) set b.tactic

source

def Lean.Elab.Tactic.getCurrMacroScope :

Lean.Elab.Tactic.TacticM Lean.MacroScope

Equations

Lean.Elab.Tactic.getCurrMacroScope = do let a ← readThe Lean.Elab.Term.Context pure a.currMacroScope

source

def Lean.Elab.Tactic.getMainModule :

Lean.Elab.Tactic.TacticM Lean.Name

Equations

Lean.Elab.Tactic.getMainModule = do let a ← Lean.getEnv pure (Lean.Environment.mainModule a)

source

unsafe def Lean.Elab.Tactic.mkTacticAttribute :

IO (Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Tactic)

Equations

Lean.Elab.Tactic.mkTacticAttribute = Lean.Elab.mkElabAttribute Lean.Elab.Tactic.Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic"

source

constant Lean.Elab.Tactic.tacticElabAttribute :

Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Tactic

source

def Lean.Elab.Tactic.mkTacticInfo (mctxBefore : Lean.MetavarContext) (goalsBefore : List Lean.MVarId) (stx : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Lean.Elab.Info

Equations

Lean.Elab.Tactic.mkTacticInfo mctxBefore goalsBefore stx = do let a ← read let a_1 ← Lean.getMCtx let a_2 ← Lean.Elab.Tactic.getUnsolvedGoals pure (Lean.Elab.Info.ofTacticInfo { toElabInfo := { elaborator := a.elaborator, stx := stx }, mctxBefore := mctxBefore, goalsBefore := goalsBefore, mctxAfter := a_1, goalsAfter := a_2 })

source

def Lean.Elab.Tactic.mkInitialTacticInfo (stx : Lean.Syntax) :

Lean.Elab.Tactic.TacticM (Lean.Elab.Tactic.TacticM Lean.Elab.Info)

Equations

Lean.Elab.Tactic.mkInitialTacticInfo stx = do let mctxBefore ← Lean.getMCtx let goalsBefore ← Lean.Elab.Tactic.getUnsolvedGoals pure (Lean.Elab.Tactic.mkTacticInfo mctxBefore goalsBefore stx)

source

@[inline]

def Lean.Elab.Tactic.withTacticInfoContext {α : Type} (stx : Lean.Syntax) (x : Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.withTacticInfoContext stx x = do let a ← Lean.Elab.Tactic.mkInitialTacticInfo stx Lean.Elab.withInfoContext x a

source

partial def Lean.Elab.Tactic.expandTacticMacroFns (stx : Lean.Syntax) (macros : List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Macro)) :

Lean.Elab.Tactic.TacticM Unit

source

partial def Lean.Elab.Tactic.expandTacticMacroFns.loop (stx : Lean.Syntax) :

List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Macro) → Lean.Elab.Tactic.TacticM Unit

source

partial def Lean.Elab.Tactic.expandTacticMacro (stx : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Unit

source

partial def Lean.Elab.Tactic.evalTacticAux (stx : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Unit

source

partial def Lean.Elab.Tactic.evalTactic (stx : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Unit

source

def Lean.Elab.Tactic.throwNoGoalsToBeSolved {α : Type} :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.throwNoGoalsToBeSolved = Lean.throwError (Lean.toMessageData "no goals to be solved")

source

def Lean.Elab.Tactic.done :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.done = do let gs ← Lean.Elab.Tactic.getUnsolvedGoals if List.isEmpty gs = true then pure PUnit.unit else do liftM (Lean.Elab.Term.reportUnsolvedGoals gs) Lean.Elab.throwAbortTactic

source

def Lean.Elab.Tactic.focus {α : Type} (x : Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.focus x = do let discr ← Lean.Elab.Tactic.getUnsolvedGoals match discr with | mvarId :: mvarIds => do Lean.Elab.Tactic.setGoals [mvarId] let a ← x let mvarIds' ← Lean.Elab.Tactic.getUnsolvedGoals Lean.Elab.Tactic.setGoals (mvarIds' ++ mvarIds) pure a | x => Lean.Elab.Tactic.throwNoGoalsToBeSolved

source

def Lean.Elab.Tactic.focusAndDone {α : Type} (tactic : Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.focusAndDone tactic = Lean.Elab.Tactic.focus do let a ← tactic Lean.Elab.Tactic.done pure a

source

def Lean.Elab.Tactic.closeUsingOrAdmit (tac : Lean.Elab.Tactic.TacticM Unit) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.closeUsingOrAdmit tac = do let discr ← Lean.Elab.Tactic.getUnsolvedGoals match discr with | mvarId :: mvarIds => tryCatch (Lean.Elab.Tactic.focusAndDone tac) fun ex => do Lean.Elab.logException ex liftM (Lean.Elab.admitGoal mvarId) Lean.Elab.Tactic.setGoals mvarIds | x => Lean.Elab.Tactic.throwNoGoalsToBeSolved

source

instance Lean.Elab.Tactic.instMonadBacktrackSavedStateTacticM :

Lean.MonadBacktrack Lean.Elab.Tactic.SavedState Lean.Elab.Tactic.TacticM

Equations

Lean.Elab.Tactic.instMonadBacktrackSavedStateTacticM = { saveState := Lean.Elab.Tactic.saveState, restoreState := fun b => Lean.Elab.Tactic.SavedState.restore b }

source

@[inline]

def Lean.Elab.Tactic.tryCatch {α : Type} (x : Lean.Elab.Tactic.TacticM α) (h : Lean.Exception → Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.tryCatch x h = do let b ← Lean.saveState tryCatch x fun ex => do Lean.Elab.Tactic.SavedState.restore b h ex

source

instance Lean.Elab.Tactic.instMonadExceptExceptionTacticM :

MonadExcept Lean.Exception Lean.Elab.Tactic.TacticM

Equations

Lean.Elab.Tactic.instMonadExceptExceptionTacticM = { throw := fun {α} => throw, tryCatch := fun {α} => Lean.Elab.Tactic.tryCatch }

source

@[inline]

def Lean.Elab.Tactic.orElse {α : Type} (x : Lean.Elab.Tactic.TacticM α) (y : Unit → Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.orElse x y = tryCatch x fun x => y ()

source

instance Lean.Elab.Tactic.instOrElseTacticM {α : Type} :

OrElse (Lean.Elab.Tactic.TacticM α)

Equations

Lean.Elab.Tactic.instOrElseTacticM = { orElse := Lean.Elab.Tactic.orElse }

source

instance Lean.Elab.Tactic.instAlternativeTacticM :

Alternative Lean.Elab.Tactic.TacticM

Equations

Lean.Elab.Tactic.instAlternativeTacticM = Alternative.mk (fun {α} => Lean.throwError (Lean.toMessageData "failed")) fun {α} => Lean.Elab.Tactic.orElse

source

def Lean.Elab.Tactic.saveTacticInfoForToken (stx : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.saveTacticInfoForToken stx = if Option.isNone (Lean.Syntax.getPos? stx) = true then pure PUnit.unit else Lean.Elab.Tactic.withTacticInfoContext stx (pure ())

source

@[inline]

def Lean.Elab.Tactic.withMacroExpansion {α : Type} (beforeStx : Lean.Syntax) (afterStx : Lean.Syntax) (x : Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.withMacroExpansion beforeStx afterStx x = Lean.Elab.withMacroExpansionInfo beforeStx afterStx (withTheReader Lean.Elab.Term.Context (fun ctx => { fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?, macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone, errToSorry := ctx.errToSorry, autoBoundImplicit := ctx.autoBoundImplicit, autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars, sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda, isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := ctx.ignoreTCFailures }) x)

source

def Lean.Elab.Tactic.adaptExpander (exp : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Syntax) :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.adaptExpander exp stx = do let stx' ← exp stx Lean.Elab.Tactic.withMacroExpansion stx stx' (Lean.Elab.Tactic.evalTactic stx')

source

def Lean.Elab.Tactic.appendGoals (mvarIds : List Lean.MVarId) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.appendGoals mvarIds = modify fun s => { goals := s.goals ++ mvarIds }

source

def Lean.Elab.Tactic.replaceMainGoal (mvarIds : List Lean.MVarId) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.replaceMainGoal mvarIds = do let discr ← Lean.Elab.Tactic.getGoals match discr with | mvarId :: mvarIds' => modify fun s => { goals := mvarIds ++ mvarIds' } | x => Lean.Elab.Tactic.throwNoGoalsToBeSolved

source

def Lean.Elab.Tactic.getMainGoal :

Lean.Elab.Tactic.TacticM Lean.MVarId

Equations

Lean.Elab.Tactic.getMainGoal = (fun loop => do let a ← Lean.Elab.Tactic.getGoals loop a) Lean.Elab.Tactic.getMainGoal.loop

source

def Lean.Elab.Tactic.getMainGoal.loop :

List Lean.MVarId → Lean.Elab.Tactic.TacticM Lean.MVarId

Equations

Lean.Elab.Tactic.getMainGoal.loop [] = Lean.Elab.Tactic.throwNoGoalsToBeSolved
Lean.Elab.Tactic.getMainGoal.loop (mvarId :: mvarIds) = do let a ← liftM (Lean.Meta.isExprMVarAssigned mvarId) if a = true then Lean.Elab.Tactic.getMainGoal.loop mvarIds else do Lean.Elab.Tactic.setGoals (mvarId :: mvarIds) pure mvarId

source

def Lean.Elab.Tactic.getMainDecl :

Lean.Elab.Tactic.TacticM Lean.MetavarDecl

Equations

Lean.Elab.Tactic.getMainDecl = do let a ← Lean.Elab.Tactic.getMainGoal liftM (Lean.Meta.getMVarDecl a)

source

def Lean.Elab.Tactic.getMainTag :

Lean.Elab.Tactic.TacticM Lean.Name

Equations

Lean.Elab.Tactic.getMainTag = do let a ← Lean.Elab.Tactic.getMainDecl pure a.userName

source

def Lean.Elab.Tactic.getMainTarget :

Lean.Elab.Tactic.TacticM Lean.Expr

Equations

Lean.Elab.Tactic.getMainTarget = do let a ← Lean.Elab.Tactic.getMainDecl liftM (Lean.Meta.instantiateMVars a.type)

source

def Lean.Elab.Tactic.withMainContext {α : Type} (x : Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.withMainContext x = do let a ← Lean.Elab.Tactic.getMainGoal Lean.Meta.withMVarContext a x

source

def Lean.Elab.Tactic.evalTacticAt (tac : Lean.Syntax) (mvarId : Lean.MVarId) :

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

Equations

Lean.Elab.Tactic.evalTacticAt tac mvarId = do let gs ← Lean.Elab.Tactic.getGoals tryFinally (do Lean.Elab.Tactic.setGoals [mvarId] Lean.Elab.Tactic.evalTactic tac Lean.Elab.Tactic.pruneSolvedGoals Lean.Elab.Tactic.getGoals) (Lean.Elab.Tactic.setGoals gs)

source

def Lean.Elab.Tactic.ensureHasNoMVars (e : Lean.Expr) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.ensureHasNoMVars e = do let e ← liftM (Lean.Meta.instantiateMVars e) let pendingMVars ← liftM (Lean.Meta.getMVars e) discard (liftM (Lean.Elab.Term.logUnassignedUsingErrorInfos pendingMVars none)) if Lean.Expr.hasExprMVar e = true then Lean.throwError (Lean.toMessageData "tactic failed, resulting expression contains metavariables" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "") else pure PUnit.unit

source

def Lean.Elab.Tactic.closeMainGoal (val : Lean.Expr) (checkUnassigned : optParam Bool true) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.closeMainGoal val checkUnassigned = let _do_jp := fun y => do let a ← Lean.Elab.Tactic.getMainGoal liftM (Lean.Meta.assignExprMVar a val) Lean.Elab.Tactic.replaceMainGoal []; if checkUnassigned = true then do let y ← Lean.Elab.Tactic.ensureHasNoMVars val _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

@[inline]

def Lean.Elab.Tactic.liftMetaMAtMain {α : Type} (x : Lean.MVarId → Lean.MetaM α) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.liftMetaMAtMain x = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainGoal liftM (x a)

source

@[inline]

def Lean.Elab.Tactic.liftMetaTacticAux {α : Type} (tac : Lean.MVarId → Lean.MetaM (α × List Lean.MVarId)) :

Lean.Elab.Tactic.TacticM α

Equations

Lean.Elab.Tactic.liftMetaTacticAux tac = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainGoal let discr ← liftM (tac a) let x : α × List Lean.MVarId := discr match x with | (a, mvarIds) => do Lean.Elab.Tactic.replaceMainGoal mvarIds pure a

source

@[inline]

def Lean.Elab.Tactic.liftMetaTactic (tactic : Lean.MVarId → Lean.MetaM (List Lean.MVarId)) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.liftMetaTactic tactic = Lean.Elab.Tactic.liftMetaTacticAux fun mvarId => do let gs ← tactic mvarId pure ((), gs)

source

@[inline]

def Lean.Elab.Tactic.liftMetaTactic1 (tactic : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.liftMetaTactic1 tactic = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainGoal let a ← liftM (tactic a) match a with | some mvarId => Lean.Elab.Tactic.replaceMainGoal [mvarId] | x => Lean.Elab.Tactic.replaceMainGoal []

source

def Lean.Elab.Tactic.tryTactic? {α : Type} (tactic : Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM (Option α)

Equations

Lean.Elab.Tactic.tryTactic? tactic = tryCatch (do let a ← tactic pure (some a)) fun x => pure none

source

def Lean.Elab.Tactic.tryTactic {α : Type} (tactic : Lean.Elab.Tactic.TacticM α) :

Lean.Elab.Tactic.TacticM Bool

Equations

Lean.Elab.Tactic.tryTactic tactic = tryCatch (do discard tactic pure true) fun x => pure false

source

def Lean.Elab.Tactic.tagUntaggedGoals (parentTag : Lean.Name) (newSuffix : Lean.Name) (newGoals : List Lean.MVarId) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.tagUntaggedGoals parentTag newSuffix newGoals = do let mctx ← Lean.getMCtx let numAnonymous : Nat := 0 let r ← forIn newGoals numAnonymous fun g r => let numAnonymous := r; if Lean.MetavarContext.isAnonymousMVar mctx g = true then let numAnonymous := numAnonymous + 1; do pure PUnit.unit pure (ForInStep.yield numAnonymous) else do pure PUnit.unit pure (ForInStep.yield numAnonymous) let x : Nat := r let numAnonymous : Nat := x Lean.modifyMCtx fun mctx => Id.run (let mctx := mctx; let idx := 1; do let r ← forIn newGoals { fst := mctx, snd := idx } fun g r => let mctx := r.fst; let idx := r.snd; if Lean.MetavarContext.isAnonymousMVar mctx g = true then let _do_jp := fun mctx idx y => let idx := idx + 1; do pure PUnit.unit pure (ForInStep.yield { fst := mctx, snd := idx }); if (numAnonymous == 1) = true then let mctx := Lean.MetavarContext.renameMVar mctx g parentTag; do let y ← pure PUnit.unit _do_jp mctx idx y else let mctx := Lean.MetavarContext.renameMVar mctx g (parentTag ++ Lean.Name.appendIndexAfter newSuffix idx); do let y ← pure PUnit.unit _do_jp mctx idx y else do pure PUnit.unit pure (ForInStep.yield { fst := mctx, snd := idx }) let x : MProd Lean.MetavarContext Nat := r match x with | { fst := mctx, snd := idx } => pure mctx)

source

def Lean.Elab.Tactic.getNameOfIdent' (id : Lean.Syntax) :

Lean.Name

Equations

Lean.Elab.Tactic.getNameOfIdent' id = if Lean.Syntax.isIdent id = true then Lean.Syntax.getId id else `_

source

def Lean.Elab.Tactic.withCaseRef {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadRef m] (arrow : Lean.Syntax) (body : Lean.Syntax) (x : m α) :

m α

Equations

Lean.Elab.Tactic.withCaseRef arrow body x = Lean.withRef (Lean.mkNullNode #[arrow, body]) x