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

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

@[implicit_reducible]

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

Equations

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

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

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

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

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

Equations

• Lean.Elab.Tactic.Grind.instBEqDSimpArgs.beq { fvarIds := a, zetaDeltaAll := a_1 } { fvarIds := b, zetaDeltaAll := b_1 } = (a == b && a_1 == b_1)
• Lean.Elab.Tactic.Grind.instBEqDSimpArgs.beq x✝¹ x✝ = false

@[implicit_reducible]

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

Equations

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

@[implicit_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 } = mixHash (mixHash 0 (hash a)) (hash a_1)

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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)

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

@[implicit_reducible, always_inline]

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

Equations

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

@[implicit_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")

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

@[implicit_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 ()

@[implicit_reducible]

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

Equations

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

@[implicit_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.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) : 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 α) (sym : Bool := false) : TacticM (α × State)

Equations

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