Documentation

Lean.Meta.Tactic.Simp.SimpTheorems

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
name? is mainly relevant for producing trace messages. It is also viewed an id used to "erase" simp theorems from SimpTheorems.
name? : Option Lean.Name
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.

def Lean.Meta.SimpTheorem.getName (s : Lean.Meta.SimpTheorem) :

Equations

Lean.Meta.SimpTheorem.getName s = match s.name? with | some n => n | none => Lean.Name.mkSimple "<unknown>"

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.

instance Lean.Meta.instToMessageDataSimpTheorem:

Lean.ToMessageData Lean.Meta.SimpTheorem

Equations

Lean.Meta.instToMessageDataSimpTheorem = { toMessageData := fun s => Lean.MessageData.ofFormat (Lean.format s) }

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 : Std.PHashSet Lean.Name
toUnfold : Std.PHashSet Lean.Name
erased : Std.PHashSet Lean.Name
toUnfoldThms : Std.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 : Std.PHashSet Lean.Name) :

Std.PHashSet Lean.Name

Equations

Lean.Meta.addSimpTheoremEntry.updateLemmaNames e s = match e.name? with | none => s | some name => Std.PersistentHashSet.insert s name

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) :

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

Equations

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

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

Equations

Lean.Meta.SimpTheorems.isLemma d declName = Std.PersistentHashSet.contains d.lemmaNames declName

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) (declName : Lean.Name) :

Lean.Meta.SimpTheorems

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

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) :

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 = Std.HashMap Lean.Name Lean.Meta.SimpExtension

opaque Lean.Meta.simpExtensionMapRef:

IO.Ref Lean.Meta.SimpExtensionMap

def Lean.Meta.registerSimpAttr (attrName : Lean.Name) (attrDescr : String) (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 (Std.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

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 (levelParams : Array Lean.Name) (proof : Lean.Expr) (post : optParam Bool true) (inv : optParam Bool false) (prio : optParam Nat 1000) (name? : optParam (Option Lean.Name) none) :

Lean.MetaM (Array Lean.Meta.SimpTheorem)

Equations

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

def Lean.Meta.SimpTheorems.add (s : Lean.Meta.SimpTheorems) (levelParams : Array Lean.Name) (proof : Lean.Expr) (inv : optParam Bool false) (post : optParam Bool true) (prio : optParam Nat 1000) (name? : optParam (Option Lean.Name) none) :

Lean.MetaM Lean.Meta.SimpTheorems

Equations

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

def Lean.Meta.SimpTheorems.add.getName? (name? : optParam (Option Lean.Name) none) (e : Lean.Expr) :

Lean.MetaM (Option Lean.Name)

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) (h : Lean.Expr) (name? : optParam (Option Lean.Name) none) :

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.Name) :

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.Name) :

Equations

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

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

Equations

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

def Lean.Meta.commandRegister_simp_attr__:

Lean.ParserDescr

Equations

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