Documentation

Lean.Meta.CongrTheorems

inductive Lean.Meta.CongrArgKind:

Type

fixed: Lean.Meta.CongrArgKind
fixedNoParam: Lean.Meta.CongrArgKind
eq: Lean.Meta.CongrArgKind
cast: Lean.Meta.CongrArgKind
heq: Lean.Meta.CongrArgKind
subsingletonInst: Lean.Meta.CongrArgKind

instance Lean.Meta.instInhabitedCongrArgKind:

Inhabited Lean.Meta.CongrArgKind

Equations

Lean.Meta.instInhabitedCongrArgKind = { default := Lean.Meta.CongrArgKind.fixed }

structure Lean.Meta.CongrTheorem:

Type

def Lean.Meta.mkHCongrWithArity (f : Lean.Expr) (numArgs : Nat) :

Lean.MetaM Lean.Meta.CongrTheorem

Equations

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

def Lean.Meta.mkHCongrWithArity.withNewEqs {α : Type} (xs : Array Lean.Expr) (ys : Array Lean.Expr) (k : Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α) :

Equations

Lean.Meta.mkHCongrWithArity.withNewEqs xs ys k = Lean.Meta.mkHCongrWithArity.withNewEqs.loop xs ys k 0 #[] #[]

partial def Lean.Meta.mkHCongrWithArity.withNewEqs.loop {α : Type} (xs : Array Lean.Expr) (ys : Array Lean.Expr) (k : Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α) (i : Nat) (eqs : Array Lean.Expr) (kinds : Array Lean.Meta.CongrArgKind) :

partial def Lean.Meta.mkHCongrWithArity.mkProof (type : Lean.Expr) :

Lean.MetaM Lean.Expr

def Lean.Meta.mkHCongr (f : Lean.Expr) :

Lean.MetaM Lean.Meta.CongrTheorem

Equations

Lean.Meta.mkHCongr f = do let a ← Lean.Meta.getFunInfo f Lean.Meta.mkHCongrWithArity f (Lean.Meta.FunInfo.getArity a)

def Lean.Meta.getCongrSimpKinds (info : Lean.Meta.FunInfo) :

Array Lean.Meta.CongrArgKind

Equations

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

def Lean.Meta.mkCongrSimpCore? (f : Lean.Expr) (info : Lean.Meta.FunInfo) (kinds : Array Lean.Meta.CongrArgKind) :

Lean.MetaM (Option Lean.Meta.CongrTheorem)

Create a congruence theorem that is useful for the simplifier.

Equations

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

def Lean.Meta.mkCongrSimpCore?.mk? (f : Lean.Expr) (info : Lean.Meta.FunInfo) (kinds : Array Lean.Meta.CongrArgKind) :

Lean.MetaM (Option Lean.Meta.CongrTheorem)

Create a congruence theorem that is useful for the simplifier. In this kind of theorem, if the i-th argument is a cast argument, then the theorem contains an input a_i representing the i-th argument in the left-hand-side, and it appears with a cast (e.g., Eq.drec ... a_i ...) in the right-hand-side. The idea is that the right-hand-side of this theorem "tells" the simplifier how the resulting term looks like.

Equations

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

partial def Lean.Meta.mkCongrSimpCore?.mk?.go (f : Lean.Expr) (info : Lean.Meta.FunInfo) (kinds : Array Lean.Meta.CongrArgKind) (lhss : Array Lean.Expr) (i : Nat) (rhss : Array Lean.Expr) (eqs : Array (Option Lean.Expr)) (hyps : Array Lean.Expr) :

Lean.MetaM Lean.Meta.CongrTheorem

def Lean.Meta.mkCongrSimpCore?.mkProof (type : Lean.Expr) (kinds : Array Lean.Meta.CongrArgKind) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkCongrSimpCore?.mkProof type kinds = Lean.Meta.mkCongrSimpCore?.mkProof.go kinds 0 type

partial def Lean.Meta.mkCongrSimpCore?.mkProof.go (kinds : Array Lean.Meta.CongrArgKind) (i : Nat) (type : Lean.Expr) :

Lean.MetaM Lean.Expr

def Lean.Meta.mkCongrSimp? (f : Lean.Expr) :

Lean.MetaM (Option Lean.Meta.CongrTheorem)

Equations

Lean.Meta.mkCongrSimp? f = do let info ← Lean.Meta.getFunInfo f Lean.Meta.mkCongrSimpCore? f info (Lean.Meta.getCongrSimpKinds info)