# 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
Equations
Instances For
def Lean.Meta.mkHCongrWithArity (f : Lean.Expr) (numArgs : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.mkHCongrWithArity.withNewEqs {α : Type} (xs : ) (ys : ) (k : ) :
Equations
Instances For
partial def Lean.Meta.mkHCongrWithArity.withNewEqs.loop {α : Type} (xs : ) (ys : ) (k : ) (i : Nat) (eqs : ) (kinds : ) :
Equations
Instances For

Compute CongrArgKinds for a simp congruence theorem.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
partial def Lean.Meta.mkCongrSimpCore?.mk?.go (subsingletonInstImplicitRhs : ) (f : Lean.Expr) (info : Lean.Meta.FunInfo) (kinds : ) (lhss : ) (i : Nat) (rhss : ) (eqs : ) (hyps : ) :
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.

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