inductive Lean.Meta.Origin : Type

An Origin is an identifier for simp theorems which indicates roughly what action the user took which lead to this theorem existing in the simp set.

• decl (declName : Name) (post : Bool := true) (inv : Bool := false) : Origin

  A global declaration in the environment.

• fvar (fvarId : FVarId) : Origin

  A local hypothesis. When contextual := true is enabled, this fvar may exist in an extension of the current local context; it will not be used for rewriting by simp once it is out of scope but it may end up in the usedSimps trace.

• stx (id : Name) (ref : Syntax) : Origin

  A proof term provided directly to a call to simp [ref, ...] where ref is the provided simp argument (of kind Parser.Tactic.simpLemma). The id is a unique identifier for the call.

• other (name : Name) : Origin

  Some other origin. name should not collide with the other types for erasure to work correctly, and simp trace will ignore this lemma. The other origins should be preferred if possible.

instance Lean.Meta.instInhabitedOrigin : Inhabited Origin

instance Lean.Meta.instReprOrigin : Repr Origin

def Lean.Meta.Origin.key : Origin → Name

A unique identifier corresponding to the origin.

def Lean.Meta.Origin.converse : Origin → Option Origin

The origin corresponding to the converse direction (← thm vs. thm)

instance Lean.Meta.instBEqOrigin : BEq Origin

instance Lean.Meta.instHashableOrigin : Hashable Origin

def Lean.Meta.Origin.lt : Origin → Origin → Bool

instance Lean.Meta.instLTOrigin : LT Origin

instance Lean.Meta.instDecidableLtOrigin (a b : Origin) : Decidable (a < b)

@[reducible, inline]

abbrev Lean.Meta.SimpTheoremKey : Type

structure Lean.Meta.SimpTheorem : Type

The fields levelParams and proof are used to encode the proof of the simp theorem. If the proof is a global declaration c, we store Expr.const c [] at proof without the universe levels, and levelParams is set to #[] When using the lemma, we create fresh universe metavariables. Motivation: most simp theorems are global declarations, and this approach is faster and saves memory.

The field levelParams is not empty only when we elaborate an expression provided by the user, and it contains universe metavariables. Then, we use abstractMVars to abstract the universe metavariables and create new fresh universe parameters that are stored at the field levelParams.

• keys : Array SimpTheoremKey
• levelParams : Array Name

  It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When proof is just a constant, we can use the universe parameter names stored in the declaration.

• proof : Expr
• priority : Nat
• post : Bool
• perm : Bool

  perm is true if lhs and rhs are identical modulo permutation of variables.

• origin : Origin

  origin is mainly relevant for producing trace messages. It is also viewed an id used to "erase" simp theorems from SimpTheorems.

• rfl : Bool

  rfl is true if proof is by Eq.refl or rfl.

  NOTE: As the visibility of proof may have changed between the point of declaration and use of a @[simp] theorem, isRfl must be used to check for this flag.

instance Lean.Meta.instInhabitedSimpTheorem : Inhabited SimpTheorem

def Lean.Meta.SimpTheorem.isRfl (s : SimpTheorem) (env : Environment) : Bool

Checks whether the theorem holds by reflexivity in the scope given by the environment.

def Lean.Meta.isRflTheorem (declName : Name) : CoreM Bool

def Lean.Meta.isRflProof (proof : Expr) : MetaM Bool

instance Lean.Meta.instToFormatSimpTheorem : ToFormat SimpTheorem

def Lean.Meta.ppOrigin {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData

def Lean.Meta.ppSimpTheorem {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData

instance Lean.Meta.instBEqSimpTheorem : BEq SimpTheorem

@[reducible, inline]

abbrev Lean.Meta.SimpTheoremTree : Type

structure Lean.Meta.SimpTheorems : Type

The theorems in a simp set.

• pre : SimpTheoremTree
• post : SimpTheoremTree
• lemmaNames : PHashSet Origin
• toUnfold : PHashSet Name

  Constants (and let-declaration FVarId) to unfold. When zetaDelta := false, the simplifier will expand a let-declaration if it is in this set.

• erased : PHashSet Origin
• toUnfoldThms : PHashMap Name (Array Name)

instance Lean.Meta.instInhabitedSimpTheorems : Inhabited SimpTheorems

def Lean.Meta.simpGlobalConfig : ConfigWithKey

Configuration for MetaM used to process global simp theorems

@[inline]

def Lean.Meta.withSimpGlobalConfig {α : Type} : MetaM α → MetaM α

partial def Lean.Meta.SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpTheorems

def Lean.Meta.addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems

def Lean.Meta.addSimpTheoremEntry.updateLemmaNames (e : SimpTheorem) (s : PHashSet Origin) : PHashSet Origin

def Lean.Meta.SimpTheorems.addDeclToUnfoldCore (d : SimpTheorems) (declName : Name) : SimpTheorems

def Lean.Meta.SimpTheorems.addLetDeclToUnfold (d : SimpTheorems) (fvarId : FVarId) : SimpTheorems

def Lean.Meta.SimpTheorems.isDeclToUnfold (d : SimpTheorems) (declName : Name) : Bool

Return true if declName is tagged to be unfolded using unfoldDefinition? (i.e., without using equational theorems).

def Lean.Meta.SimpTheorems.isLetDeclToUnfold (d : SimpTheorems) (fvarId : FVarId) : Bool

def Lean.Meta.SimpTheorems.isLemma (d : SimpTheorems) (thmId : Origin) : Bool

def Lean.Meta.SimpTheorems.registerDeclToUnfoldThms (d : SimpTheorems) (declName : Name) (eqThms : Array Name) : SimpTheorems

Register the equational theorems for the given definition.

def Lean.Meta.SimpTheorems.erase {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems

inductive Lean.Meta.SimpEntry : Type

• thm : SimpTheorem → SimpEntry
• toUnfold : Name → SimpEntry
• toUnfoldThms : Name → Array Name → SimpEntry

instance Lean.Meta.instInhabitedSimpEntry : Inhabited SimpEntry

@[reducible, inline]

abbrev Lean.Meta.SimpExtension : Type

The environment extension that contains a simp set, returned by Lean.Meta.registerSimpAttr.

Use the simp set's attribute or Lean.Meta.addSimpTheorem to add theorems to the simp set. Use Lean.Meta.SimpExtension.getTheorems to get the contents.

def Lean.Meta.SimpExtension.getTheorems (ext : SimpExtension) : CoreM SimpTheorems

def Lean.Meta.addSimpTheorem (ext : SimpExtension) (declName : Name) (post inv : Bool) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit

def Lean.Meta.mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension

@[reducible, inline]

abbrev Lean.Meta.SimpExtensionMap : Type

opaque Lean.Meta.simpExtensionMapRef : IO.Ref SimpExtensionMap

def Lean.Meta.getSimpExtension? (attrName : Name) : IO (Option SimpExtension)

def Lean.Meta.SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post : Bool := true) (inv : Bool := false) (prio : Nat := 1000) : MetaM SimpTheorems

Auxiliary method for adding a global declaration to a SimpTheorems datastructure.

def Lean.Meta.SimpTheorem.getValue (simpThm : SimpTheorem) : MetaM Expr

def Lean.Meta.SimpTheorems.ignoreEquations (declName : Name) : CoreM Bool

Reducible functions and projection functions should always be put in toUnfold, instead of trying to use equational theorems.

The simplifiers has special support for structure and class projections, and gets confused when they suddenly rewrite, so ignore equations for them

def Lean.Meta.SimpTheorems.unfoldEvenWithEqns (declName : Name) : CoreM Bool

Even if a function has equation theorems, we also store it in the toUnfold set in the following two cases: 1- It was defined by structural recursion and has a smart-unfolding associated declaration. 2- It is non-recursive.

Reason: unfoldPartialApp := true or conditional equations may not apply.

Remark: In the future, we are planning to disable this behavior unless unfoldPartialApp := true. Moreover, users will have to use f.eq_def if they want to force the definition to be unfolded.

def Lean.Meta.SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems

def Lean.Meta.SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name) (proof : Expr) (inv : Bool := false) (post : Bool := true) (prio : Nat := 1000) (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheorems

Auxiliary method for adding a local simp theorem to a SimpTheorems datastructure.

@[reducible, inline]

abbrev Lean.Meta.SimpTheoremsArray : Type

def Lean.Meta.SimpTheoremsArray.addTheorem (thmsArray : SimpTheoremsArray) (id : Origin) (h : Expr) (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheoremsArray

def Lean.Meta.SimpTheoremsArray.eraseTheorem (thmsArray : SimpTheoremsArray) (thmId : Origin) : SimpTheoremsArray

def Lean.Meta.SimpTheoremsArray.isErased (thmsArray : SimpTheoremsArray) (thmId : Origin) : Bool

def Lean.Meta.SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName : Name) : Bool

def Lean.Meta.SimpTheoremsArray.isLetDeclToUnfold (thmsArray : SimpTheoremsArray) (fvarId : FVarId) : Bool