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

Equations

• Lean.Meta.instInhabitedCongrArgKind = { default := Lean.Meta.instInhabitedCongrArgKind.default }

def Lean.Meta.instInhabitedCongrArgKind.default : CongrArgKind

Equations

• Lean.Meta.instInhabitedCongrArgKind.default = Lean.Meta.CongrArgKind.fixed

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

Equations

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

instance Lean.Meta.instReprCongrArgKind : Repr CongrArgKind

Equations

• Lean.Meta.instReprCongrArgKind = { reprPrec := Lean.Meta.instReprCongrArgKind.repr }

instance Lean.Meta.instBEqCongrArgKind : BEq CongrArgKind

Equations

• Lean.Meta.instBEqCongrArgKind = { beq := Lean.Meta.instBEqCongrArgKind.beq }

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

Equations

• Lean.Meta.instBEqCongrArgKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Lean.Meta.CongrTheorem : Type

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

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

Equations

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

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

Equations

• Lean.Meta.mkHCongr f = do let __do_lift ← Lean.Meta.getFunInfo f Lean.Meta.mkHCongrWithArity f __do_lift.getArity

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

Computes CongrArgKinds for a simp congruence theorem.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

def Lean.Meta.hcongrThmSuffixBase : String

Equations

• Lean.Meta.hcongrThmSuffixBase = "hcongr"

def Lean.Meta.hcongrThmSuffixBasePrefix : String

Equations

• Lean.Meta.hcongrThmSuffixBasePrefix = Lean.Meta.hcongrThmSuffixBase ++ "_"

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

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

Equations

• Lean.Meta.isHCongrReservedNameSuffix s = (Lean.Meta.hcongrThmSuffixBasePrefix.isPrefixOf s && (s.drop 7).isNat)

def Lean.Meta.congrSimpSuffix : String

Equations

• Lean.Meta.congrSimpSuffix = "congr_simp"

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.

Equations

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

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.

Equations

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