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

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

inductive Lean.Elab.Tactic.Grind.ExtraTheorem : Type

An extra theorem passed to simp in sym => mode.

• const (declName : Name) : ExtraTheorem
• fvar (fvarId : FVarId) : ExtraTheorem

def Lean.Elab.Tactic.Grind.instBEqExtraTheorem.beq : ExtraTheorem → ExtraTheorem → Bool

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instBEqExtraTheorem : BEq ExtraTheorem

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instHashableExtraTheorem : Hashable ExtraTheorem

def Lean.Elab.Tactic.Grind.instHashableExtraTheorem.hash : ExtraTheorem → UInt64

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

Cache key for Sym.simp variant invocations.

• variant : Name
• extras : Array ExtraTheorem

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instBEqSimpCacheKey : BEq SimpCacheKey

def Lean.Elab.Tactic.Grind.instBEqSimpCacheKey.beq : SimpCacheKey → SimpCacheKey → Bool

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instHashableSimpCacheKey : Hashable SimpCacheKey

def Lean.Elab.Tactic.Grind.instHashableSimpCacheKey.hash : SimpCacheKey → UInt64

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

• fvarIds : Array FVarId
• zetaDeltaAll : Bool

def Lean.Elab.Tactic.Grind.instBEqDSimpArgs.beq : DSimpArgs → DSimpArgs → Bool

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instBEqDSimpArgs : BEq DSimpArgs

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instHashableDSimpArgs : Hashable DSimpArgs

def Lean.Elab.Tactic.Grind.instHashableDSimpArgs.hash : DSimpArgs → UInt64

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

Cache key for Sym.dsimp variant invocations.

• variant : Name
• args : DSimpArgs

def Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey.beq : DSimpCacheKey → DSimpCacheKey → Bool

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey : BEq DSimpCacheKey

@[implicit_reducible]

instance Lean.Elab.Tactic.Grind.instHashableDSimpCacheKey : Hashable DSimpCacheKey

def Lean.Elab.Tactic.Grind.instHashableDSimpCacheKey.hash : DSimpCacheKey → UInt64

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

• backwardRuleName : PHashMap Name Meta.Sym.BackwardRule

  Cache for BackwardRules created from declaration names (sym mode only).

• backwardRuleSyntax : PHashMap (Nat × Nat) Meta.Sym.BackwardRule

  Cache for BackwardRules created from elaborated terms, keyed by syntax byte position range (sym mode only).

• simpState : Std.HashMap SimpCacheKey Meta.Sym.Simp.State

  Per-variant persistent Sym.simp cache. Keyed by variant name + extra theorem names.

• dsimpState : Std.HashMap DSimpCacheKey Meta.Sym.DSimp.State

  Per-variant persistent Sym.dsimp cache. Keyed by variant name + args.

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

• symState : Meta.Sym.State
• grindState : Meta.Grind.State
• goals : List Meta.Grind.Goal
• cache : Cache

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

• term : Term.SavedState
• tactic : State

@[reducible, inline]

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

@[reducible, inline]

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

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

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

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

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

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

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

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

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

@[implicit_reducible, always_inline]

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

@[implicit_reducible]

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

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

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

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

@[inline]

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

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 α

@[implicit_reducible]

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

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.

@[inline]

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

Non-backtracking try/catch.

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

@[implicit_reducible]

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

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

Execute x with error recovery disabled

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

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

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

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

@[inline]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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 ;

@[inline]

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

Elaborate x with stx on the macro stack

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

Adapt a syntax transformation to a regular tactic evaluator.

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

Return the first goal.

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

Execute x using the main goal local context and instances

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

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

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

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

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

inductive Lean.Elab.Tactic.Grind.LiftActionCoreResult : Type

• closed : LiftActionCoreResult
• subgoals : LiftActionCoreResult

def Lean.Elab.Tactic.Grind.liftActionCore (a : Meta.Grind.Action) : GrindTacticM LiftActionCoreResult

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

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

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.

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

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

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

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

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