inductive Lean.Meta.Origin : Type

• A global declaration in the environment.

  decl: Lean.Name → Lean.Meta.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.

  fvar: Lean.FVarId → Lean.Meta.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.

  stx: Lean.Name → Lean.Syntax → Lean.Meta.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.

  other: Lean.Name → Lean.Meta.Origin

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.

instance Lean.Meta.instInhabitedOrigin : Inhabited Lean.Meta.Origin

Equations

• Lean.Meta.instInhabitedOrigin = { default := Lean.Meta.Origin.decl default }

instance Lean.Meta.instReprOrigin : Repr Lean.Meta.Origin

Equations

• Lean.Meta.instReprOrigin = { reprPrec := Lean.Meta.reprOrigin✝ }

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

A unique identifier corresponding to the origin.

Equations

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

instance Lean.Meta.instBEqOrigin : BEq Lean.Meta.Origin

Equations

• Lean.Meta.instBEqOrigin = { beq := fun a a_1 => Lean.Meta.Origin.key a == Lean.Meta.Origin.key a_1 }

instance Lean.Meta.instHashableOrigin : Hashable Lean.Meta.Origin

Equations

• Lean.Meta.instHashableOrigin = { hash := fun a => hash (Lean.Meta.Origin.key a) }

structure Lean.Meta.SimpTheorem : Type

• keys : Array Lean.Meta.DiscrTree.Key

• 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.

  levelParams : Array Lean.Name
• proof : Lean.Expr
• priority : Nat
• post : Bool

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

  perm : Bool

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

  origin : Lean.Meta.Origin

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

  rfl : Bool

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.

instance Lean.Meta.instInhabitedSimpTheorem : Inhabited Lean.Meta.SimpTheorem

Equations

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

partial def Lean.Meta.isRflProofCore (type : Lean.Expr) (proof : Lean.Expr) : Lean.CoreM Bool

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

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

Equations

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

instance Lean.Meta.instToFormatSimpTheorem : Lean.ToFormat Lean.Meta.SimpTheorem

Equations

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

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

Equations

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

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

Equations

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

instance Lean.Meta.instBEqSimpTheorem : BEq Lean.Meta.SimpTheorem

Equations

• Lean.Meta.instBEqSimpTheorem = { beq := fun e₁ e₂ => e₁.proof == e₂.proof }

structure Lean.Meta.SimpTheorems : Type

• pre : Lean.Meta.DiscrTree Lean.Meta.SimpTheorem
• post : Lean.Meta.DiscrTree Lean.Meta.SimpTheorem
• lemmaNames : Lean.PHashSet Lean.Meta.Origin
• toUnfold : Lean.PHashSet Lean.Name
• erased : Lean.PHashSet Lean.Meta.Origin
• toUnfoldThms : Lean.PHashMap Lean.Name (Array Lean.Name)

instance Lean.Meta.instInhabitedSimpTheorems : Inhabited Lean.Meta.SimpTheorems

Equations

• Lean.Meta.instInhabitedSimpTheorems = { default := { pre := default, post := default, lemmaNames := default, toUnfold := default, erased := default, toUnfoldThms := default } }

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

Equations

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

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

Equations

• Lean.Meta.addSimpTheoremEntry.updateLemmaNames e s = Lean.PersistentHashSet.insert s e.origin

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

Equations

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

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

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

Equations

• Lean.Meta.SimpTheorems.isDeclToUnfold d declName = Lean.PersistentHashSet.contains d.toUnfold declName

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

Equations

• Lean.Meta.SimpTheorems.isLemma d thmId = Lean.PersistentHashSet.contains d.lemmaNames thmId

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

Register the equational theorems for the given definition.

Equations

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

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

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

Equations

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

inductive Lean.Meta.SimpEntry : Type

• thm: Lean.Meta.SimpTheorem → Lean.Meta.SimpEntry
• toUnfold: Lean.Name → Lean.Meta.SimpEntry
• toUnfoldThms: Lean.Name → Array Lean.Name → Lean.Meta.SimpEntry

instance Lean.Meta.instInhabitedSimpEntry : Inhabited Lean.Meta.SimpEntry

Equations

• Lean.Meta.instInhabitedSimpEntry = { default := Lean.Meta.SimpEntry.thm default }

@[inline]

abbrev Lean.Meta.SimpExtension : Type

Equations

• Lean.Meta.SimpExtension = Lean.SimpleScopedEnvExtension Lean.Meta.SimpEntry Lean.Meta.SimpTheorems

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

Equations

• Lean.Meta.SimpExtension.getTheorems ext = do let a ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext a)

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

Equations

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

def Lean.Meta.mkSimpAttr (attrName : Lean.Name) (attrDescr : String) (ext : Lean.Meta.SimpExtension) (ref : autoParam Lean.Name _auto✝) : IO Unit

Equations

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

def Lean.Meta.mkSimpExt (extName : Lean.Name) : IO Lean.Meta.SimpExtension

Equations

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

@[inline]

abbrev Lean.Meta.SimpExtensionMap : Type

Equations

• Lean.Meta.SimpExtensionMap = Lean.HashMap Lean.Name Lean.Meta.SimpExtension

opaque Lean.Meta.simpExtensionMapRef : IO.Ref Lean.Meta.SimpExtensionMap

def Lean.Meta.registerSimpAttr (attrName : Lean.Name) (attrDescr : String) (ref : autoParam Lean.Name _auto✝) (extName : optParam Lean.Name (Lean.Name.appendAfter attrName "Ext")) : IO Lean.Meta.SimpExtension

Equations

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

opaque Lean.Meta.simpExtension : Lean.Meta.SimpExtension

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

Equations

• Lean.Meta.getSimpExtension? attrName = do let a ← ST.Ref.get Lean.Meta.simpExtensionMapRef pure (Lean.HashMap.find? a attrName)

def Lean.Meta.getSimpTheorems : Lean.CoreM Lean.Meta.SimpTheorems

Equations

• Lean.Meta.getSimpTheorems = Lean.Meta.SimpExtension.getTheorems Lean.Meta.simpExtension

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

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

Equations

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

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

Equations

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

def Lean.Meta.mkSimpTheorems (id : Lean.Meta.Origin) (levelParams : Array Lean.Name) (proof : Lean.Expr) (post : optParam Bool true) (inv : optParam Bool false) (prio : optParam Nat 1000) : Lean.MetaM (Array Lean.Meta.SimpTheorem)

Auxiliary method for creating simp theorems from a proof term val.

Equations

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

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

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

Equations

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

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

Equations

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

@[inline]

abbrev Lean.Meta.SimpTheoremsArray : Type

Equations

• Lean.Meta.SimpTheoremsArray = Array Lean.Meta.SimpTheorems

def Lean.Meta.SimpTheoremsArray.addTheorem (thmsArray : Lean.Meta.SimpTheoremsArray) (id : Lean.Meta.Origin) (h : Lean.Expr) : Lean.MetaM Lean.Meta.SimpTheoremsArray

Equations

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

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

Equations

• Lean.Meta.SimpTheoremsArray.eraseTheorem thmsArray thmId = Array.map (fun thms => Lean.Meta.SimpTheorems.eraseCore thms thmId) thmsArray

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

Equations

• Lean.Meta.SimpTheoremsArray.isErased thmsArray thmId = Array.any thmsArray (fun thms => Lean.PersistentHashSet.contains thms.erased thmId) 0 (Array.size thmsArray)

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

Equations

• Lean.Meta.SimpTheoremsArray.isDeclToUnfold thmsArray declName = Array.any thmsArray (fun thms => Lean.Meta.SimpTheorems.isDeclToUnfold thms declName) 0 (Array.size thmsArray)

def Lean.Parser.Command.registerSimpAttr : Lean.ParserDescr

Equations

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