def Lean.Elab.Tactic.elabSimpConfigCore : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.Config

Equations

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

def Lean.Elab.Tactic.elabSimpConfigCtxCore : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.ConfigCtx

Equations

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

def Lean.Elab.Tactic.elabDSimpConfigCore : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.DSimp.Config

Equations

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

inductive Lean.Elab.Tactic.SimpKind : Type

• simp: Lean.Elab.Tactic.SimpKind
• simpAll: Lean.Elab.Tactic.SimpKind
• dsimp: Lean.Elab.Tactic.SimpKind

instance Lean.Elab.Tactic.instInhabitedSimpKind : Inhabited Lean.Elab.Tactic.SimpKind

Equations

• Lean.Elab.Tactic.instInhabitedSimpKind = { default := Lean.Elab.Tactic.SimpKind.simp }

instance Lean.Elab.Tactic.instBEqSimpKind : BEq Lean.Elab.Tactic.SimpKind

Equations

• Lean.Elab.Tactic.instBEqSimpKind = { beq := Lean.Elab.Tactic.beqSimpKind✝ }

def Lean.Elab.Tactic.tacticToDischarge (tacticCode : Lean.Syntax) : Lean.Elab.Tactic.TacticM (IO.Ref Lean.Elab.Term.State × Lean.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.

Equations

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

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

• default: Lean.Elab.Tactic.Simp.DischargeWrapper
• custom: IO.Ref Lean.Elab.Term.State → Lean.Meta.Simp.Discharge → Lean.Elab.Tactic.Simp.DischargeWrapper

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Simp.DischargeWrapper.default.with x = x none

def Lean.Elab.Tactic.elabSimpConfig (optConfig : Lean.Syntax) (kind : Lean.Elab.Tactic.SimpKind) : Lean.Elab.TermElabM Lean.Meta.Simp.Config

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.elabSimpConfig optConfig Lean.Elab.Tactic.SimpKind.simp = Lean.Elab.Tactic.elabSimpConfigCore optConfig
• Lean.Elab.Tactic.elabSimpConfig optConfig Lean.Elab.Tactic.SimpKind.simpAll = do let __do_lift ← Lean.Elab.Tactic.elabSimpConfigCtxCore optConfig pure __do_lift.toConfig

structure Lean.Elab.Tactic.ElabSimpArgsResult : Type

• ctx : Lean.Meta.Simp.Context
• simprocs : Lean.Meta.Simp.SimprocsArray
• starArg : Bool

inductive Lean.Elab.Tactic.ResolveSimpIdResult : Type

• none: Lean.Elab.Tactic.ResolveSimpIdResult
• expr: Lean.Expr → Lean.Elab.Tactic.ResolveSimpIdResult
• simproc: Lake.Name → Lean.Elab.Tactic.ResolveSimpIdResult
• ext: (ext₁? : Option Lean.Meta.SimpExtension) → (ext₂? : Option Lean.Meta.Simp.SimprocExtension) → (ext₁?.isSome || ext₂?.isSome) = true → Lean.Elab.Tactic.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.

def Lean.Elab.Tactic.elabSimpArgs (stx : Lean.Syntax) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (eraseLocal : Bool) (kind : Lean.Elab.Tactic.SimpKind) : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.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.

Equations

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

def Lean.Elab.Tactic.elabSimpArgs.isSimproc? (e : Lean.Expr) : Lean.MetaM (Option Lake.Name)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.elabSimpArgs.isSimproc? e = pure none

def Lean.Elab.Tactic.elabSimpArgs.resolveSimpIdTheorem? (simpArgTerm : Lean.Term) : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.ResolveSimpIdResult

Equations

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

@[inline]

def Lean.Elab.Tactic.simpOnlyBuiltins : List Lake.Name

Equations

• Lean.Elab.Tactic.simpOnlyBuiltins = [`eq_self, `iff_self]

structure Lean.Elab.Tactic.MkSimpContextResult : Type

• ctx : Lean.Meta.Simp.Context
• simprocs : Lean.Meta.Simp.SimprocsArray
• dischargeWrapper : Lean.Elab.Tactic.Simp.DischargeWrapper

def Lean.Elab.Tactic.mkSimpContext (stx : Lean.Syntax) (eraseLocal : Bool) (kind : optParam Lean.Elab.Tactic.SimpKind Lean.Elab.Tactic.SimpKind.simp) (ignoreStarArg : optParam Bool false) (simpTheorems : optParam (Lean.CoreM Lean.Meta.SimpTheorems) Lean.Meta.getSimpTheorems) : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.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.

Equations

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

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

def Lean.Elab.Tactic.mkSimpOnly (stx : Lean.Syntax) (usedSimps : Lean.Meta.Simp.UsedSimps) : Lean.MetaM Lean.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.

Equations

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

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

Equations

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

def Lean.Elab.Tactic.simpLocation (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (loc : Lean.Elab.Tactic.Location) : Lean.Elab.Tactic.TacticM Lean.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.

Equations

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

def Lean.Elab.Tactic.simpLocation.go (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats

Equations

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

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

Equations

• Lean.Elab.Tactic.withSimpDiagnostics x = do let stats ← x liftM (Lean.Meta.Simp.reportDiag stats)

def Lean.Elab.Tactic.evalSimp : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalSimpAll : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

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

def Lean.Elab.Tactic.dsimpLocation.go (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Lean.Elab.Tactic.evalDSimp : Lean.Elab.Tactic.Tactic

Equations

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

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? : Lean.Syntax → Option (Array Lean.Syntax)

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

Equations

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

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

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

Equations

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