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

instance Lean.Meta.instReprCongrArgKind : Repr CongrArgKind

instance Lean.Meta.instBEqCongrArgKind : BEq CongrArgKind

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.mkHCongrWithArity.withNewEqs {α : Type} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α

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

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

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

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

Compute 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 CongrArgKind.eq, and otherwise it is CongrArgKind.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)

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

def Lean.Meta.mkCongrSimpCore?.mk? (subsingletonInstImplicitRhs : Bool := true) (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option 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.

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

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

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

def Lean.Meta.mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) : 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.