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 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 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.getCongrSimpKindsForArgZero (info : Lean.Meta.FunInfo) : Lean.MetaM (Array Lean.Meta.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.

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 : 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 : 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 : 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 : 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.