structure Lean.Elab.Tactic.Grind.Context extends 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

Equations

• Lean.Elab.Tactic.Grind.instBEqExtraTheorem.beq (Lean.Elab.Tactic.Grind.ExtraTheorem.const a) (Lean.Elab.Tactic.Grind.ExtraTheorem.const b) = (a == b)
• Lean.Elab.Tactic.Grind.instBEqExtraTheorem.beq (Lean.Elab.Tactic.Grind.ExtraTheorem.fvar a) (Lean.Elab.Tactic.Grind.ExtraTheorem.fvar b) = (a == b)
• Lean.Elab.Tactic.Grind.instBEqExtraTheorem.beq x✝¹ x✝ = false

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instBEqExtraTheorem = { beq := Lean.Elab.Tactic.Grind.instBEqExtraTheorem.beq }

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instHashableExtraTheorem = { hash := Lean.Elab.Tactic.Grind.instHashableExtraTheorem.hash }

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

Equations

• Lean.Elab.Tactic.Grind.instHashableExtraTheorem.hash (Lean.Elab.Tactic.Grind.ExtraTheorem.const a) = mixHash 0 (hash a)
• Lean.Elab.Tactic.Grind.instHashableExtraTheorem.hash (Lean.Elab.Tactic.Grind.ExtraTheorem.fvar a) = mixHash 1 (hash a)

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

Cache key for Sym.simp variant invocations.

• variant : Name
• extras : Array ExtraTheorem

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instBEqSimpCacheKey = { beq := Lean.Elab.Tactic.Grind.instBEqSimpCacheKey.beq }

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

Equations

• Lean.Elab.Tactic.Grind.instBEqSimpCacheKey.beq { variant := a, extras := a_1 } { variant := b, extras := b_1 } = (a == b && a_1 == b_1)
• Lean.Elab.Tactic.Grind.instBEqSimpCacheKey.beq x✝¹ x✝ = false

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instHashableSimpCacheKey = { hash := Lean.Elab.Tactic.Grind.instHashableSimpCacheKey.hash }

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

Equations

• Lean.Elab.Tactic.Grind.instHashableSimpCacheKey.hash { variant := a, extras := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

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

• fvarIds : Array FVarId
• zetaDeltaAll : Bool
• declNames : Array Name

  Global declarations: definitions to unfold and rfl-theorems to rewrite with.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Grind.instBEqDSimpArgs.beq x✝¹ x✝ = false

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instBEqDSimpArgs = { beq := Lean.Elab.Tactic.Grind.instBEqDSimpArgs.beq }

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instHashableDSimpArgs = { hash := Lean.Elab.Tactic.Grind.instHashableDSimpArgs.hash }

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

Equations

• Lean.Elab.Tactic.Grind.instHashableDSimpArgs.hash { fvarIds := a, zetaDeltaAll := a_1, declNames := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

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

Cache key for Sym.dsimp variant invocations.

• variant : Name
• args : DSimpArgs

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey = { beq := Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey.beq }

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

Equations

• Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey.beq { variant := a, args := a_1 } { variant := b, args := b_1 } = (a == b && a_1 == b_1)
• Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey.beq x✝¹ x✝ = false

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

Equations

• Lean.Elab.Tactic.Grind.instHashableDSimpCacheKey.hash { variant := a, args := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Grind.instHashableDSimpCacheKey = { hash := Lean.Elab.Tactic.Grind.instHashableDSimpCacheKey.hash }

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

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) => { symState := s.symState, grindState := s.grindState, goals := goals, cache := s.cache }

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

@[instance_reducible, always_inline]

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

Equations

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

@[instance_reducible]

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_reducible]

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_reducible]

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_reducible]

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

Equations

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

@[instance_reducible]

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 () 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.liftSymM {α : Type} (k : Meta.Sym.SymM α) : GrindTacticM α

Lifts a SymM computation into GrindTacticM.

Equations

• Lean.Elab.Tactic.Grind.liftSymM k = Lean.Elab.Tactic.Grind.liftGrindM (liftM k)

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

Throws an error unless the tactic is being executed in sym => mode.

Equations

• Lean.Elab.Tactic.Grind.ensureSym = do let __do_lift ← read if __do_lift.sym = true then pure () else Lean.throwError (Lean.toMessageData "tactic is only available in `sym =>` mode")

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.

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

• closed : LiftActionCoreResult
• subgoals : LiftActionCoreResult

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

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

• Lean.Elab.Tactic.Grind.liftAction a = discard (Lean.Elab.Tactic.Grind.liftActionCore a)

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) (sym : Bool) : TermElabM (Meta.Grind.Goal → TSyntax `grind → Meta.Grind.GrindM (List Meta.Grind.Goal))

Creates the evaluator used to replay grind scripts from GrindM (e.g., Action.checkSeqAt). The returned function runs a script at the given goal in a fresh GrindTacticM context and returns the remaining goals.

The context must mirror the one the script will run in when pasted by the user. In particular, sym must be set in sym => mode, otherwise scripts containing sym-only steps such as intros and by_contra are rejected.

Equations

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

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

Equations

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

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

Equations

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