Documentation

Lean.Meta.Tactic.Simp.SimpCongrTheorems

structure Lean.Meta.SimpCongrTheorem :

Data for user-defined theorems marked with the congr attribute.

This type should be confused with CongrTheorem which represents different kinds of automatically generated congruence theorems. The simp tactic also uses some of them.

theoremName : Name
funName : Name
hypothesesPos : Array Nat
priority : Nat

Instances For

instance Lean.Meta.instInhabitedSimpCongrTheorem :

Inhabited SimpCongrTheorem

Equations

Lean.Meta.instInhabitedSimpCongrTheorem = { default := { theoremName := default, funName := default, hypothesesPos := default, priority := default } }

instance Lean.Meta.instReprSimpCongrTheorem :

Repr SimpCongrTheorem

Equations

Lean.Meta.instReprSimpCongrTheorem = { reprPrec := Lean.Meta.reprSimpCongrTheorem✝ }

structure Lean.Meta.SimpCongrTheorems :

lemmas : SMap Name (List SimpCongrTheorem)

Instances For

instance Lean.Meta.instInhabitedSimpCongrTheorems :

Inhabited SimpCongrTheorems

Equations

Lean.Meta.instInhabitedSimpCongrTheorems = { default := { lemmas := default } }

instance Lean.Meta.instReprSimpCongrTheorems :

Repr SimpCongrTheorems

Equations

Lean.Meta.instReprSimpCongrTheorems = { reprPrec := Lean.Meta.reprSimpCongrTheorems✝ }

def Lean.Meta.SimpCongrTheorems.get (d : SimpCongrTheorems) (declName : Name) :

List SimpCongrTheorem

Equations

d.get declName = match d.lemmas.find? declName with | none => [] | some cs => cs

def Lean.Meta.addSimpCongrTheoremEntry (d : SimpCongrTheorems) (e : SimpCongrTheorem) :

SimpCongrTheorems

Equations

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

def Lean.Meta.addSimpCongrTheoremEntry.insert (e : SimpCongrTheorem) :

List SimpCongrTheorem → List SimpCongrTheorem

Equations

Lean.Meta.addSimpCongrTheoremEntry.insert e [] = [e]
Lean.Meta.addSimpCongrTheoremEntry.insert e (e' :: es) = if e.priority ≥ e'.priority then e :: e' :: es else e' :: Lean.Meta.addSimpCongrTheoremEntry.insert e es

opaque Lean.Meta.congrExtension :

SimpleScopedEnvExtension SimpCongrTheorem SimpCongrTheorems

def Lean.Meta.mkSimpCongrTheorem (declName : Name) (prio : Nat) :

MetaM SimpCongrTheorem

Equations

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

def Lean.Meta.mkSimpCongrTheorem.onlyMVarsAt (t : Expr) (mvarSet : MVarIdSet) :

Return true if t contains a metavariable that is not in mvarSet

Equations

Lean.Meta.mkSimpCongrTheorem.onlyMVarsAt t mvarSet = (Lean.Expr.find? (fun (e : Lean.Expr) => e.isMVar && !Lean.RBTree.contains mvarSet e.mvarId!) t).isNone

def Lean.Meta.addSimpCongrTheorem (declName : Name) (attrKind : AttributeKind) (prio : Nat) :

Equations

Lean.Meta.addSimpCongrTheorem declName attrKind prio = do let lemma ← Lean.Meta.mkSimpCongrTheorem declName prio Lean.ScopedEnvExtension.add Lean.Meta.congrExtension lemma attrKind

def Lean.Meta.getSimpCongrTheorems :

CoreM SimpCongrTheorems

Equations

Lean.Meta.getSimpCongrTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.congrExtension __do_lift)