structure Lean.Meta.Simp.ConfigWithOptionsextends Lean.Meta.Simp.Config : Type

Configuration for simp, for supporting tactic configuration option syntax.

• maxSteps : Nat
• maxDischargeDepth : Nat
• contextual : Bool
• memoize : Bool
• singlePass : Bool
• zeta : Bool
• beta : Bool
• eta : Bool
• etaStruct : EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• arith : Bool
• autoUnfold : Bool
• dsimp : Bool
• failIfUnchanged : Bool
• ground : Bool
• unfoldPartialApp : Bool
• zetaDelta : Bool
• index : Bool
• implicitDefEqProofs : Bool
• zetaUnused : Bool
• catchRuntime : Bool
• zetaHave : Bool
• letToHave : Bool
• congrConsts : Bool
• bitVecOfNat : Bool
• warnExponents : Bool
• suggestions : Bool
• maxSuggestions : Option Nat
• locals : Bool
• instances : Bool
• userConfig : Options

  User options. Registering a global option tactic.simp.user.myOption enables the tactic configurations (user.myOption := ...) and +user.myOption.

structure Lean.Meta.DSimp.ConfigWithOptionsextends Lean.Meta.DSimp.Config : Type

Configuration for dsimp, for supporting tactic configuration option syntax.

• zeta : Bool
• beta : Bool
• eta : Bool
• etaStruct : EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• autoUnfold : Bool
• failIfUnchanged : Bool
• unfoldPartialApp : Bool
• zetaDelta : Bool
• index : Bool
• zetaUnused : Bool
• zetaHave : Bool
• locals : Bool
• instances : Bool
• userConfig : Options

  User options. Registering a global option tactic.simp.user.myOption enables the tactic configurations (user.myOption := ...) and +user.myOption.

def Lean.Elab.Tactic.elabSimpConfigCore (optConfig : Syntax) (initConfig : Meta.Simp.Config := { }) (initUserConfig : Options := ∅) : TacticM Meta.Simp.ConfigWithOptions

def Lean.Elab.Tactic.elabSimpConfigCtxCore (optConfig : Syntax) (initConfig : Meta.Simp.ConfigCtx := { }) (initUserConfig : Options := ∅) : TacticM Meta.Simp.ConfigWithOptions

opaque Lean.Elab.Tactic.tactic.simp.user.exampleBool : Lean.Option Bool

opaque Lean.Elab.Tactic.tactic.simp.user.exampleNat : Lean.Option Nat

opaque Lean.Elab.Tactic.tactic.simp.user.exampleInt : Lean.Option Int

opaque Lean.Elab.Tactic.tactic.simp.user.exampleString : Lean.Option String

inductive Lean.Elab.Tactic.SimpKind : Type

• simp : SimpKind
• simpAll : SimpKind
• dsimp : SimpKind

@[implicit_reducible]

instance Lean.Elab.Tactic.instInhabitedSimpKind : Inhabited SimpKind

def Lean.Elab.Tactic.instBEqSimpKind.beq : SimpKind → SimpKind → Bool

@[implicit_reducible]

instance Lean.Elab.Tactic.instBEqSimpKind : BEq SimpKind

def Lean.Elab.Tactic.tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Meta.Simp.Discharge)

Implement a simp discharge function using the given tactic syntax code. Recall that simp dischargers are in SimpM which does not have access to Term.State. We need access to Term.State to store messages and update the info tree. Thus, we create an IO.ref to track these changes at Term.State when we execute tacticCode. We must set this reference with the current Term.State before we execute simp using the generated Simp.Discharge.

inductive Lean.Elab.Tactic.Simp.DischargeWrapper : Type

• default : DischargeWrapper
• custom (ref : IO.Ref Term.State) (discharge : Meta.Simp.Discharge) : DischargeWrapper

def Lean.Elab.Tactic.Simp.DischargeWrapper.with {α : Type} (w : DischargeWrapper) (x : Option Meta.Simp.Discharge → TacticM α) : TacticM α

def Lean.Elab.Tactic.elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.ConfigWithOptions

inductive Lean.Elab.Tactic.ResolveSimpIdResult : Type

• none : ResolveSimpIdResult
• expr (e : Expr) : ResolveSimpIdResult
• simproc (declName : Name) : ResolveSimpIdResult
• ext (ext₁? : Option Meta.SimpExtension) (ext₂? : Option Meta.Simp.SimprocExtension) (h : (ext₁?.isSome || ext₂?.isSome) = true) : ResolveSimpIdResult

  Recall that when we declare a simp attribute using register_simp_attr, we automatically create a simproc attribute. However, if the user creates simp and simproc attributes programmatically, then one of them may be missing. Moreover, when we write simp [seval], we want to retrieve both the simp and simproc sets. We want to hide from users that simp and simproc sets are stored in different data-structures.

inductive Lean.Elab.Tactic.ElabSimpArgResult : Type

The result of elaborating a single simp argument

• addEntries (entries : Array Meta.SimpEntry) : ElabSimpArgResult
• addSimproc («simproc» : Name) (post : Bool) : ElabSimpArgResult
• addLetToUnfold (fvarId : FVarId) : ElabSimpArgResult
• ext (ext₁? : Option Meta.SimpExtension) (ext₂? : Option Meta.Simp.SimprocExtension) (h : (ext₁?.isSome || ext₂?.isSome) = true) : ElabSimpArgResult
• erase (toErase : Meta.Origin) : ElabSimpArgResult
• eraseSimproc (toErase : Name) : ElabSimpArgResult
• star : ElabSimpArgResult
• none : ElabSimpArgResult

def Lean.Elab.Tactic.ElabSimpArgResult.simpTheorems : ElabSimpArgResult → Array Meta.SimpTheorem

structure Lean.Elab.Tactic.ElabSimpArgsResult : Type

The result of elaborating a full array of simp arguments and applying them to the simp context.

• ctx : Meta.Simp.Context
• simprocs : Meta.Simp.SimprocsArray
• simpArgs : Array (Syntax × ElabSimpArgResult)

  The elaborated simp arguments with syntax

def Lean.Elab.Tactic.elabSimpArgs (stx : Syntax) (ctx : Meta.Simp.Context) (simprocs : Meta.Simp.SimprocsArray) (eraseLocal : Bool) (kind : SimpKind) (ignoreStarArg : Bool := false) : TacticM ElabSimpArgsResult

Elaborate extra simp theorems provided to simp. stx is of the form "[" simpTheorem,* "]" If eraseLocal == true, then we consider local declarations when resolving names for erased theorems (- id), this option only makes sense for simp_all or * is used. When recover := true, try to recover from errors as much as possible so that users keep seeing the current goal.

def Lean.Elab.Tactic.simpParamsPos : Nat

Position for the [..] child syntax in the simp tactic.

def Lean.Elab.Tactic.simpOnlyPos : Nat

Position for the only child syntax in the simp tactic.

def Lean.Elab.Tactic.isSimpOnly (stx : TSyntax `tactic) : Bool

def Lean.Elab.Tactic.getSimpParams (stx : TSyntax `tactic) : Array Syntax

def Lean.Elab.Tactic.setSimpParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic

@[inline]

def Lean.Elab.Tactic.simpOnlyBuiltins : List Name

structure Lean.Elab.Tactic.MkSimpContextResult : Type

• ctx : Meta.Simp.Context
• simprocs : Meta.Simp.SimprocsArray
• dischargeWrapper : Simp.DischargeWrapper
• simpArgs : Array (Syntax × ElabSimpArgResult)

  The elaborated simp arguments with syntax

def Lean.Elab.Tactic.elabSimpLocals (thms : Meta.SimpTheorems) (kind : SimpKind) : MetaM Meta.SimpTheorems

Add all definitions from the current file to unfold.

def Lean.Elab.Tactic.mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind : SimpKind := SimpKind.simp) (ignoreStarArg : Bool := false) (simpTheorems : CoreM Meta.SimpTheorems := Meta.getSimpTheorems) : TacticM MkSimpContextResult

Create the Simp.Context for the simp, dsimp, and simp_all tactics. If kind != SimpKind.simp, the discharge option must be none

TODO: generate error message if non rfl theorems are provided as arguments to dsimp.

The argument simpTheorems defaults to getSimpTheorems, but allows overriding with an arbitrary mechanism to choose the simp theorems besides those specified in the syntax. Note that if the syntax includes simp only, the simpTheorems argument is ignored.

@[inline]

def Lean.Elab.Tactic.withLoopChecking {m : Type → Type} {α : Type} [Monad m] [MonadExcept Exception m] [MonadRuntimeException m] [MonadLiftT MetaM m] (r : MkSimpContextResult) (k : m α) : m α

Runs the given action. If it throws a maxRecDepth exception (nested or not), run the loop checking. If it does not throw, run the loop checking only if explicitly enabled.

opaque Lean.Elab.Tactic.tactic.simp.trace : Lean.Option Bool

def Lean.Elab.Tactic.mkSimpOnly (stx : Syntax) (usedSimps : Meta.Simp.UsedSimps) : MetaM Syntax

If stx is the syntax of a simp, simp_all or dsimp tactic invocation, and usedSimps is the set of simp lemmas used by this invocation, then mkSimpOnly creates the syntax of an equivalent simp only, simp_all only or dsimp only invocation.

def Lean.Elab.Tactic.traceSimpCall (stx : Syntax) (usedSimps : Meta.Simp.UsedSimps) : MetaM Unit

opaque Lean.Elab.Tactic.linter.unusedSimpArgs : Lean.Option Bool

structure Lean.Elab.Tactic.UnusedSimpArgsInfo : Type

• mask : Array Bool

@[implicit_reducible]

instance Lean.Elab.Tactic.instTypeNameUnusedSimpArgsInfo : TypeName UnusedSimpArgsInfo

def Lean.Elab.Tactic.pushUnusedSimpArgsInfo {m : Type → Type} [Monad m] [MonadInfoTree m] (simpStx : Syntax) (mask : Array Bool) : m Unit

def Lean.Elab.Tactic.warnUnusedSimpArgs (simpArgs : Array (Syntax × ElabSimpArgResult)) (usedSimps : Meta.Simp.UsedSimps) : MetaM Unit

Checks the simp arguments for unused ones, and stores a bitmask of unused ones in the info tree, to be picked up by the linter. (This indirection is necessary because the same simp syntax may be executed multiple times, and different simp arguments may be used in each step.)

def Lean.Elab.Tactic.simpLocation (ctx : Meta.Simp.Context) (simprocs : Meta.Simp.SimprocsArray) (discharge? : Option Meta.Simp.Discharge := none) (loc : Location) : TacticM Meta.Simp.Stats

simpLocation ctx discharge? varIdToLemmaId loc runs the simplifier at locations specified by loc, using the simp theorems collected in ctx optionally running a discharger specified in discharge? on generated subgoals.

Its primary use is as the implementation of the simp [...] at ... and simp only [...] at ... syntaxes, but can also be used by other tactics when a Syntax is not available.

For many tactics other than the simplifier, one should use the withLocation tactic combinator when working with a location.

def Lean.Elab.Tactic.withSimpDiagnostics (x : TacticM Meta.Simp.Diagnostics) : TacticM Unit

def Lean.Elab.Tactic.evalSimp : Tactic

def Lean.Elab.Tactic.evalSimpAll : Tactic

def Lean.Elab.Tactic.dsimpLocation (ctx : Meta.Simp.Context) (simprocs : Meta.Simp.SimprocsArray) (loc : Location) : TacticM Unit

def Lean.Elab.Tactic.evalDSimp : Tactic

The following parsers for simp arguments are not actually used at present in the implementation of simp above, but are useful for further tactics which need to parse simp arguments.

def Lean.Parser.Tactic.getSimpArgs? : Syntax → Option (Array Syntax)

Extract the arguments from a simpArgs syntax as an array of syntaxes

def Lean.Parser.Tactic.getDSimpArgs? : Syntax → Option (Array Syntax)

Extract the arguments from a dsimpArgs syntax as an array of syntaxes