Lean.Elab.Tactic.Basic

source

def Lean.Elab.admitGoal (mvarId : Lean.MVarId) :

Lean.MetaM Unit

Equations

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

source

def Lean.Elab.goalsToMessageData (goals : List Lean.MVarId) :

Lean.MessageData

Equations

Lean.Elab.goalsToMessageData goals = Lean.MessageData.joinSep (List.map Lean.MessageData.ofGoal goals) (Lean.toMessageData "\n\n")

source

def Lean.Elab.Term.reportUnsolvedGoals (goals : List Lean.MVarId) :

Lean.Elab.TermElabM Unit

Equations

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

source

structure Lean.Elab.Tactic.Context:

Type

Declaration name of the executing elaborator, used by mkTacticInfo to persist it in the info tree
elaborator : Lean.Name
If true, enable "error recovery" in some tactics. For example, cases tactic admits unsolved alternatives when recover == true. The combinator withoutRecover disables "error recovery" while executing . This is useful for tactics such as first | ... | ....
recover : Bool

source

structure Lean.Elab.Tactic.SavedState:

Type

term : Lean.Elab.Term.SavedState
tactic : Lean.Elab.Tactic.State

source

@[inline]

abbrev Lean.Elab.Tactic.TacticM (α : Type) :

Type

Equations

Lean.Elab.Tactic.TacticM = ReaderT Lean.Elab.Tactic.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.State Lean.Elab.TermElabM)

source

@[inline]

abbrev Lean.Elab.Tactic.Tactic:

Type

Equations

Lean.Elab.Tactic.Tactic = (Lean.Syntax → Lean.Elab.Tactic.TacticM Unit)

source

instance Lean.Elab.Tactic.instMonadTacticM:

Monad Lean.Elab.Tactic.TacticM

Equations

Lean.Elab.Tactic.instMonadTacticM = let i := inferInstanceAs (Monad Lean.Elab.Tactic.TacticM); Monad.mk

source

def Lean.Elab.Tactic.getGoals:

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

Equations

Lean.Elab.Tactic.getGoals = do let a ← get pure a.goals

source

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

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.setGoals mvarIds = modify fun x => { goals := mvarIds }

source

def Lean.Elab.Tactic.pruneSolvedGoals:

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.pruneSolvedGoals = do let gs ← Lean.Elab.Tactic.getGoals let gs ← List.filterM (fun g => not <$> liftM (Lean.Meta.isExprMVarAssigned g)) gs Lean.Elab.Tactic.setGoals gs

source

def Lean.Elab.Tactic.getUnsolvedGoals:

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

Equations

Lean.Elab.Tactic.getUnsolvedGoals = do Lean.Elab.Tactic.pruneSolvedGoals Lean.Elab.Tactic.getGoals

source

def Lean.Elab.Tactic.run (mvarId : Lean.MVarId) (x : Lean.Elab.Tactic.TacticM Unit) :

Lean.Elab.TermElabM (List Lean.MVarId)

Equations

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

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.Core.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

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

source

opaque 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

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

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 (s : Lean.Elab.Tactic.SavedState) (stx : Lean.Syntax) (macros : List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Macro)) :

Lean.Elab.Tactic.TacticM Unit

source

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

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

source

partial def Lean.Elab.Tactic.expandTacticMacro (s : Lean.Elab.Tactic.SavedState) (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

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

source

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

Lean.Elab.Tactic.TacticM α

Equations

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

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

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

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

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

Lean.Elab.Tactic.TacticM α

Execute x with error recovery disabled

Equations

Lean.Elab.Tactic.withoutRecover x = withReader (fun ctx => { elaborator := ctx.elaborator, recover := false }) x

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 (Lean.Elab.Tactic.withoutRecover 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 {x} => 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

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

source

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

Lean.Elab.Tactic.Tactic

Adapt a syntax transformation to a regular tactic evaluator.

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

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

source

def Lean.Elab.Tactic.getMainGoal:

Lean.Elab.Tactic.TacticM Lean.MVarId

Return the first goal.

Equations

Lean.Elab.Tactic.getMainGoal = do let a ← Lean.Elab.Tactic.getGoals Lean.Elab.Tactic.getMainGoal.loop a

source

def Lean.Elab.Tactic.getMainGoal.loop:

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

Equations

One or more equations did not get rendered due to their size.
Lean.Elab.Tactic.getMainGoal.loop [] = Lean.Elab.Tactic.throwNoGoalsToBeSolved

source

def Lean.Elab.Tactic.getMainDecl:

Lean.Elab.Tactic.TacticM Lean.MetavarDecl

Return the main goal metavariable declaration.

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

Return the main goal tag.

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

Return expected type for the main goal.

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 α

Execute x using the main goal local context and instances

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)

Evaluate tac at mvarId, and return the list of resulting subgoals.

Equations

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

source

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

Lean.Elab.Tactic.TacticM Unit

Equations

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

source

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

Lean.Elab.Tactic.TacticM Unit

Close main goal using the given expression. If checkUnassigned == true, then val must not contain unassinged metavariables.

Equations

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

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

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

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

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

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

Use parentTag to tag untagged goals at newGoals. If there are multiple new untagged goals, they are named using ._ where idx > 0. If there is only one new untagged goal, then we just use parentTag

Equations

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

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 α

Use position of => $body for error messages. If there is a line break before body, the message will be displayed on => only, but the "full range" for the info view will still include body.

Equations

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