structure Lean.Elab.Tactic.Grind.Contextextends Lean.Elab.Tactic.Context : Type

• elaborator : Name
• recover : Bool
• ctx : Meta.Grind.Context
• methods : Meta.Grind.Methods
• params : Meta.Grind.Params

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

• state : Meta.Grind.State
• goals : List Meta.Grind.Goal

structure Lean.Elab.Tactic.Grind.SavedState : Type

• term : Term.SavedState
• tactic : State

@[reducible, inline]

abbrev Lean.Elab.Tactic.Grind.GrindTacticM (α : Type) : Type

Equations

• Lean.Elab.Tactic.Grind.GrindTacticM = ReaderT Lean.Elab.Tactic.Grind.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.Grind.State Lean.Elab.TermElabM)

@[reducible, inline]

abbrev Lean.Elab.Tactic.Grind.GrindTactic : Type

Equations

• Lean.Elab.Tactic.Grind.GrindTactic = (Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM Unit)

def Lean.Elab.Tactic.Grind.getGoals : GrindTacticM (List Meta.Grind.Goal)

Returns the list of goals. Goals may or may not already be assigned.

Equations

• Lean.Elab.Tactic.Grind.getGoals = do let __do_lift ← get pure __do_lift.goals

def Lean.Elab.Tactic.Grind.setGoals (goals : List Meta.Grind.Goal) : GrindTacticM Unit

Equations

• Lean.Elab.Tactic.Grind.setGoals goals = modify fun (s : Lean.Elab.Tactic.Grind.State) => { state := s.state, goals := goals }

def Lean.Elab.Tactic.Grind.pruneSolvedGoals : GrindTacticM Unit

Equations

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

def Lean.Elab.Tactic.Grind.getUnsolvedGoals : GrindTacticM (List Meta.Grind.Goal)

Equations

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

def Lean.Elab.Tactic.Grind.getUnsolvedGoalMVarIds : GrindTacticM (List MVarId)

Equations

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

def Lean.Elab.Tactic.Grind.saveState : GrindTacticM SavedState

Equations

• Lean.Elab.Tactic.Grind.saveState = do let __do_lift ← liftM Lean.Elab.Term.saveState let __do_lift_1 ← get pure { term := __do_lift, tactic := __do_lift_1 }

def Lean.Elab.Tactic.Grind.SavedState.restore (b : SavedState) (restoreInfo : Bool := false) : GrindTacticM Unit

Equations

• b.restore restoreInfo = do liftM (b.term.restore restoreInfo) set b.tactic

@[always_inline]

instance Lean.Elab.Tactic.Grind.instMonadGrindTacticM : Monad GrindTacticM

Equations

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

instance Lean.Elab.Tactic.Grind.instInhabitedGrindTacticM {α : Type} : Inhabited (GrindTacticM α)

Equations

• Lean.Elab.Tactic.Grind.instInhabitedGrindTacticM = { default := fun (x : Lean.Elab.Tactic.Grind.Context) (x_1 : ST.Ref IO.RealWorld Lean.Elab.Tactic.Grind.State) => default }

opaque Lean.Elab.Tactic.Grind.grindTacElabAttribute : KeyedDeclsAttribute GrindTactic

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

Equations

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

def Lean.Elab.Tactic.Grind.mkInitialTacticInfo (stx : Syntax) : GrindTacticM (GrindTacticM Info)

Equations

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

@[inline]

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

Equations

• Lean.Elab.Tactic.Grind.withTacticInfoContext stx x = do let __do_lift ← Lean.Elab.Tactic.Grind.mkInitialTacticInfo stx Lean.Elab.withInfoContext x __do_lift

structure Lean.Elab.Tactic.Grind.EvalTacticFailure : Type

• exception : Exception
• state : SavedState

partial def Lean.Elab.Tactic.Grind.evalGrindTactic (stx : Syntax) : GrindTacticM Unit

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

Equations

• Lean.Elab.Tactic.Grind.throwNoGoalsToBeSolved = Lean.throwError (Lean.toMessageData "No goals to be solved")

instance Lean.Elab.Tactic.Grind.instMonadBacktrackSavedStateGrindTacticM : MonadBacktrack SavedState GrindTacticM

Equations

• Lean.Elab.Tactic.Grind.instMonadBacktrackSavedStateGrindTacticM = { saveState := Lean.Elab.Tactic.Grind.saveState, restoreState := fun (b : Lean.Elab.Tactic.Grind.SavedState) => b.restore }

def Lean.Elab.Tactic.Grind.focus {α : Type} (k : GrindTacticM α) : GrindTacticM α

Runs x with only the first unsolved goal as the goal. Fails if there are no goal to be solved.

Equations

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

@[inline]

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

Non-backtracking try/catch.

Equations

• Lean.Elab.Tactic.Grind.tryCatch x h = tryCatch x fun (ex : Lean.Exception) => h ex

@[inline]

def Lean.Elab.Tactic.Grind.tryCatchRestore {α : Type} (x : GrindTacticM α) (h : Exception → GrindTacticM α) : GrindTacticM α

Backtracking try/catch. This is used for the MonadExcept instance for GrindTacticM.

Equations

• Lean.Elab.Tactic.Grind.tryCatchRestore x h = do let b ← Lean.saveState tryCatch x fun (ex : Lean.Exception) => do b.restore h ex

instance Lean.Elab.Tactic.Grind.instMonadExceptExceptionGrindTacticM : MonadExcept Exception GrindTacticM

Equations

• Lean.Elab.Tactic.Grind.instMonadExceptExceptionGrindTacticM = { throw := fun {α : Type} => throw, tryCatch := fun {α : Type} => Lean.Elab.Tactic.Grind.tryCatchRestore }

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

Execute x with error recovery disabled

Equations

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

def Lean.Elab.Tactic.Grind.throwOrLogErrorAt (ref : Syntax) (msg : MessageData) : GrindTacticM Unit

Like throwErrorAt, but, if recovery is enabled, logs the error instead.

Equations

• Lean.Elab.Tactic.Grind.throwOrLogErrorAt ref msg = do let __do_lift ← read if __do_lift.recover = true then Lean.logErrorAt ref msg else Lean.throwErrorAt ref msg

def Lean.Elab.Tactic.Grind.throwOrLogError (msg : MessageData) : GrindTacticM Unit

Like throwError, but, if recovery is enabled, logs the error instead.

Equations

• Lean.Elab.Tactic.Grind.throwOrLogError msg = do let __do_lift ← Lean.getRef Lean.Elab.Tactic.Grind.throwOrLogErrorAt __do_lift msg

@[inline]

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

Equations

• Lean.Elab.Tactic.Grind.orElse x y = tryCatch (Lean.Elab.Tactic.Grind.withoutRecover x) fun (x : Lean.Exception) => y ()

instance Lean.Elab.Tactic.Grind.instOrElseGrindTacticM {α : Type} : OrElse (GrindTacticM α)

Equations

• Lean.Elab.Tactic.Grind.instOrElseGrindTacticM = { orElse := Lean.Elab.Tactic.Grind.orElse }

instance Lean.Elab.Tactic.Grind.instAlternativeGrindTacticM : Alternative GrindTacticM

Equations

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

def Lean.Elab.Tactic.Grind.saveTacticInfoForToken (stx : Syntax) : GrindTacticM Unit

Save the current tactic state for a token stx. This method is a no-op if stx has no position information. We use this method to save the tactic state at punctuation such as ;

Equations

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

@[inline]

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

Elaborate x with stx on the macro stack

Equations

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

def Lean.Elab.Tactic.Grind.adaptExpander (exp : Syntax → GrindTacticM Syntax) : GrindTactic

Adapt a syntax transformation to a regular tactic evaluator.

Equations

• Lean.Elab.Tactic.Grind.adaptExpander exp stx = do let stx' ← exp stx Lean.Elab.Tactic.Grind.withMacroExpansion stx stx' (Lean.Elab.Tactic.Grind.evalGrindTactic stx')

def Lean.Elab.Tactic.Grind.getMainGoal : GrindTacticM Meta.Grind.Goal

Return the first goal.

Equations

• Lean.Elab.Tactic.Grind.getMainGoal = do let __do_lift ← Lean.Elab.Tactic.Grind.getGoals Lean.Elab.Tactic.Grind.getMainGoal.loop✝ __do_lift

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

Execute x using the main goal local context and instances

Equations

• Lean.Elab.Tactic.Grind.withMainContext x = do let __do_lift ← Lean.Elab.Tactic.Grind.getMainGoal __do_lift.mvarId.withContext x

def Lean.Elab.Tactic.Grind.tryTactic? {α : Type} (tac : GrindTacticM α) : GrindTacticM (Option α)

Equations

• Lean.Elab.Tactic.Grind.tryTactic? tac = tryCatch (do let __do_lift ← tac pure (some __do_lift)) fun (x : Lean.Exception) => pure none

def Lean.Elab.Tactic.Grind.tryTactic {α : Type} (tac : GrindTacticM α) : GrindTacticM Bool

Equations

• Lean.Elab.Tactic.Grind.tryTactic tac = tryCatch (do discard tac pure true) fun (x : Lean.Exception) => pure false

def Lean.Elab.Tactic.Grind.liftGrindM {α : Type} (k : Meta.Grind.GrindM α) : GrindTacticM α

Equations

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

def Lean.Elab.Tactic.Grind.replaceMainGoal (goals : List Meta.Grind.Goal) : GrindTacticM Unit

Equations

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

def Lean.Elab.Tactic.Grind.liftGoalM {α : Type} (k : Meta.Grind.GoalM α) : GrindTacticM α

Equations

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

def Lean.Elab.Tactic.Grind.liftSearchM {α : Type} (k : Meta.Grind.SearchM α) : GrindTacticM α

Equations

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

def Lean.Elab.Tactic.Grind.liftAction (a : Meta.Grind.Action) : GrindTacticM Unit

Equations

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

def Lean.Elab.Tactic.Grind.done : GrindTacticM Unit

Equations

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

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

Runs tactic with only the first unsolved goal as the goal, and expects it leave no goals. Fails if there are no goal to be solved.

Equations

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

def Lean.Elab.Tactic.Grind.closeUsingOrAdmit (tac : GrindTacticM Unit) : GrindTacticM Unit

Close the main goal using the given tactic. If it fails, log the error and admit

Equations

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

def Lean.Elab.Tactic.Grind.GrindTacticM.run {α : Type} (x : GrindTacticM α) (ctx : Context) (s : State) : TermElabM (α × State)

Equations

• x.run ctx s = (x ctx).run s

def Lean.Elab.Tactic.Grind.mkEvalTactic' (elaborator : Name) (params : Meta.Grind.Params) : TermElabM (Meta.Grind.Goal → TSyntax `grind → Meta.Grind.GrindM (List Meta.Grind.Goal))

Equations

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

def Lean.Elab.Tactic.Grind.mkEvalTactic (params : Meta.Grind.Params) : TacticM (Meta.Grind.Goal → TSyntax `grind → Meta.Grind.GrindM (List Meta.Grind.Goal))

Equations

• Lean.Elab.Tactic.Grind.mkEvalTactic params = do let __do_lift ← read liftM (Lean.Elab.Tactic.Grind.mkEvalTactic' __do_lift.elaborator params)

def Lean.Elab.Tactic.Grind.GrindTacticM.runAtGoal {α : Type} (mvarId : MVarId) (params : Meta.Grind.Params) (k : GrindTacticM α) : TacticM (α × State)

Equations

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