inductive Lean.Meta.CongrArgKind : Type

• fixed : CongrArgKind

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

• fixedNoParam : 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 : 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 : 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 : 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 heterogeneous equality.

• subsingletonInst : CongrArgKind

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

instance Lean.Meta.instInhabitedCongrArgKind : Inhabited CongrArgKind

def Lean.Meta.instInhabitedCongrArgKind.default : CongrArgKind

def Lean.Meta.instReprCongrArgKind.repr : CongrArgKind → Nat → Format

instance Lean.Meta.instReprCongrArgKind : Repr CongrArgKind

instance Lean.Meta.instBEqCongrArgKind : BEq CongrArgKind

def Lean.Meta.instBEqCongrArgKind.beq : CongrArgKind → CongrArgKind → Bool

structure Lean.Meta.CongrTheorem : Type

• type : Expr
• proof : Expr
• argKinds : Array CongrArgKind

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

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

def Lean.Meta.getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind)

Computes CongrArgKinds for a simp congruence theorem.

def Lean.Meta.getCongrSimpKindsForArgZero (info : FunInfo) : MetaM (Array CongrArgKind)

Variant of getCongrSimpKinds for rewriting just argument 0. If it is possible to rewrite, the 0th CongrArgKind is .eq, and otherwise it is .fixed. This is used for the arg conv tactic.

def Lean.Meta.mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem)

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

def Lean.Meta.mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) (maxArgs? : Option Nat := none) : MetaM (Option CongrTheorem)

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

If subsingletonInstImplicitRhs = true, 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.

def Lean.Meta.hcongrThmSuffixBase : String

def Lean.Meta.hcongrThmSuffixBasePrefix : String

def Lean.Meta.isHCongrReservedNameSuffix (s : String) : Bool

Returns true if s is of the form hcongr_<idx>

def Lean.Meta.congrSimpSuffix : String

opaque Lean.Meta.congrKindsExt : MapDeclarationExtension (Array CongrArgKind)

def Lean.Meta.mkHCongrWithArityForConst? (declName : Name) (levels : List Level) (numArgs : Nat) : MetaM (Option CongrTheorem)

Similar to mkHCongrWithArity, but uses reserved names to ensure we don't keep creating the same congruence theorem over and over again.

def Lean.Meta.mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option CongrTheorem)

Similar to mkCongrSimp?, but uses reserved names to ensure we don't keep creating the same congruence theorem over and over again.