Documentation

Lean.Meta.Tactic.Simp.SimpCongrTheorems

structure Lean.Meta.SimpCongrTheorem:

Type

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

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

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

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 := [anonymous] }

structure Lean.Meta.SimpCongrTheorems:

Type

lemmas : Lean.SMap Lean.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 := [anonymous] }

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

List Lean.Meta.SimpCongrTheorem

Equations

Lean.Meta.SimpCongrTheorems.get d declName = match Lean.SMap.find? d.lemmas 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 : Lean.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) :

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

Equations

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

def Lean.Meta.addSimpCongrTheorem (declName : Lean.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.MetaM Lean.Meta.SimpCongrTheorems

Equations

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