inductive Lean.Meta.CongrArgKind : Type

• 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 ...]

instance Lean.Meta.instInhabitedCongrArgKind : Inhabited Lean.Meta.CongrArgKind

Equations

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

instance Lean.Meta.instReprCongrArgKind : Repr Lean.Meta.CongrArgKind

Equations

• Lean.Meta.instReprCongrArgKind = { reprPrec := Lean.Meta.reprCongrArgKind✝ }

structure Lean.Meta.CongrTheorem : Type

• type : Lean.Expr
• proof : Lean.Expr
• argKinds : Array Lean.Meta.CongrArgKind

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

Equations

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

def Lean.Meta.mkHCongrWithArity.withNewEqs {α : Type} (xs : Array Lean.Expr) (ys : Array Lean.Expr) (k : Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α) : Lean.MetaM α

Equations

• Lean.Meta.mkHCongrWithArity.withNewEqs xs ys k = Lean.Meta.mkHCongrWithArity.withNewEqs.loop xs ys k 0 #[] #[]

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

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

def Lean.Meta.mkHCongr (f : Lean.Expr) : Lean.MetaM Lean.Meta.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 : Lean.Expr) (info : Lean.Meta.FunInfo) : Lean.MetaM (Array Lean.Meta.CongrArgKind)

Compute CongrArgKinds for a simp congruence theorem.

Equations

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

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

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.

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

Equations

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

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

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

Equations

• Lean.Meta.mkCongrSimpCore?.mkProof type kinds = Lean.Meta.mkCongrSimpCore?.mkProof.go kinds 0 type

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

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