# Documentation

Lean.Meta.CongrTheorems

• fixed: Lean.Meta.CongrArgKind

It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides.

• fixedNoParam: Lean.Meta.CongrArgKind

It is not a parameter for the congruence theorem, the theorem was specialized for this parameter. This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it.

• eq: Lean.Meta.CongrArgKind

The lemma contains three parameters for this kind of argument a_i, b_i and eq_i : a_i = b_i. a_i and b_i represent the left and right hand sides, and eq_i is a proof for their equality.

• cast: Lean.Meta.CongrArgKind

The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. They correspond to arguments that are subsingletons/propositions.

• heq: Lean.Meta.CongrArgKind

The lemma contains three parameters for this kind of argument a_i, b_i and eq_i : HEq a_i b_i. a_i and b_i represent the left and right hand sides, and eq_i is a proof for their heterogeneous equality.

• subsingletonInst: Lean.Meta.CongrArgKind

For congr-simp theorems only. Indicates a decidable instance argument. The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...]

Instances For
Instances For
def Lean.Meta.mkHCongrWithArity (f : Lean.Expr) (numArgs : Nat) :
Instances For
def Lean.Meta.mkHCongrWithArity.withNewEqs {α : Type} (xs : ) (ys : ) (k : ) :
Instances For
partial def Lean.Meta.mkHCongrWithArity.withNewEqs.loop {α : Type} (xs : ) (ys : ) (k : ) (i : Nat) (eqs : ) (kinds : ) :
Instances For

Compute CongrArgKinds for a simp congruence theorem.

Instances For
def Lean.Meta.mkCongrSimpCore? (f : Lean.Expr) (info : Lean.Meta.FunInfo) (kinds : ) (subsingletonInstImplicitRhs : ) :

Create a congruence theorem that is useful for the simplifier and congr tactic.

Instances For
def Lean.Meta.mkCongrSimpCore?.mk? (subsingletonInstImplicitRhs : ) (f : Lean.Expr) (info : Lean.Meta.FunInfo) (kinds : ) :

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.

Instances For
partial def Lean.Meta.mkCongrSimpCore?.mk?.go (subsingletonInstImplicitRhs : ) (f : Lean.Expr) (info : Lean.Meta.FunInfo) (kinds : ) (lhss : ) (i : Nat) (rhss : ) (eqs : ) (hyps : ) :
Instances For
partial def Lean.Meta.mkCongrSimpCore?.mkProof.go (kinds : ) (i : Nat) (type : Lean.Expr) :
def Lean.Meta.mkCongrSimp? (f : Lean.Expr) (subsingletonInstImplicitRhs : ) :

Create a congruence theorem for f. The theorem is used in the simplifier.

If subsingletonInstImplicitRhs = true, the the rhs corresponding to [Decidable p] parameters is marked as instance implicit. It forces the simplifier to compute the new instance when applying the congruence theorem. For the congr tactic we set it to false.

Instances For