Documentation

Lean.Elab.Tactic.Simp

source
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.
source
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.
source
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.
source
inductive Lean.Elab.Tactic.SimpKind:
Type
source
instance Lean.Elab.Tactic.instInhabitedSimpKind:
Inhabited Lean.Elab.Tactic.SimpKind
Equations
source
instance Lean.Elab.Tactic.instBEqSimpKind:
BEq Lean.Elab.Tactic.SimpKind
Equations
source
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.
source
inductive Lean.Elab.Tactic.Simp.DischargeWrapper:
Type
source
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.
source
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.
source
structure Lean.Elab.Tactic.ElabSimpArgsResult:
Type
source
inductive Lean.Elab.Tactic.ResolveSimpIdResult:
Type
source
structure Lean.Elab.Tactic.MkSimpContextResult:
Type
source
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) :
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.simpLocation (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (fvarIdToLemmaId : optParam Lean.Meta.FVarIdToLemmaId ∅) (loc : Lean.Elab.Tactic.Location) :
Lean.Elab.Tactic.TacticM Unit

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. (Local hypotheses which have been added to the simp theorems must be recorded in fvarIdToLemmaId.)

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.
source
def Lean.Elab.Tactic.simpLocation.go (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalSimp:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalSimpAll:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.dsimpLocation (ctx : Lean.Meta.Simp.Context) (loc : Lean.Elab.Tactic.Location) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.dsimpLocation.go (ctx : Lean.Meta.Simp.Context) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalDSimp:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.