structure Lean.Meta.SimpCongrTheorem : Type

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 : Lake.Name
• funName : Lake.Name
• hypothesesPos : Array Nat
• priority : Nat

instance Lean.Meta.instInhabitedSimpCongrTheorem : Inhabited Lean.Meta.SimpCongrTheorem

Equations

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

instance Lean.Meta.instReprSimpCongrTheorem : Repr Lean.Meta.SimpCongrTheorem

Equations

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

structure Lean.Meta.SimpCongrTheorems : Type

• lemmas : Lean.SMap Lake.Name (List Lean.Meta.SimpCongrTheorem)

instance Lean.Meta.instInhabitedSimpCongrTheorems : Inhabited Lean.Meta.SimpCongrTheorems

Equations

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

instance Lean.Meta.instReprSimpCongrTheorems : Repr Lean.Meta.SimpCongrTheorems

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.addSimpCongrTheoremEntry.insert (e : Lean.Meta.SimpCongrTheorem) : List Lean.Meta.SimpCongrTheorem → List Lean.Meta.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 : Lean.SimpleScopedEnvExtension Lean.Meta.SimpCongrTheorem Lean.Meta.SimpCongrTheorems

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

Equations

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

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

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 : Lake.Name) (attrKind : Lean.AttributeKind) (prio : Nat) : Lean.MetaM Unit

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 : Lean.CoreM Lean.Meta.SimpCongrTheorems

Equations

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