This module provides functions to pack and unpack values using nested PProd or And, as used in the .below construction, in the .brecOn construction for mutual recursion and and the mutual_induct construction.

It uses And (equivalent to PProd.{0} when possible).

The nesting is t₁ ×' (t₂ ×' t₃), not t₁ ×' (t₂ ×' (t₃ ×' PUnit)). This is more readable, slightly shorter, and means that the packing is the identity if n=1, which we rely on in some places. It comes at the expense that hat projection needs to know n.

Packing an empty list uses True or PUnit depending on the given lvl.

Also see Lean.Meta.ArgsPacker for a similar module for PSigma and PSum, used by well-founded recursion.

def Lean.Meta.mkPProd (e1 e2 : Lean.Expr) : Lean.MetaM Lean.Expr

Given types t₁ and t₂, produces t₁ ×' t₂ (or t₁ ∧ t₂ if the universes allow)

Equations

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

def Lean.Meta.mkPProdMk (e1 e2 : Lean.Expr) : Lean.MetaM Lean.Expr

Given values of typs t₁ and t₂, produces value of type t₁ ×' t₂ (or t₁ ∧ t₂ if the universes allow)

Equations

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

def Lean.Meta.mkPProdFst (e : Lean.Expr) : Lean.MetaM Lean.Expr

PProd.fst or And.left (using .proj)

def Lean.Meta.mkPProdSnd (e : Lean.Expr) : Lean.MetaM Lean.Expr

PProd.snd or And.right (using .proj)

Equations

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

def Lean.Meta.PProdN.pack (lvl : Lean.Level) (xs : Array Lean.Expr) : Lean.MetaM Lean.Expr

Given types tᵢ, produces t₁ ×' t₂ ×' t₃

Equations

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

def Lean.Meta.PProdN.mk (lvl : Lean.Level) (xs : Array Lean.Expr) : Lean.MetaM Lean.Expr

Given values xᵢ of type tᵢ, produces value of type t₁ ×' t₂ ×' t₃

Equations

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

def Lean.Meta.PProdN.proj (n i : Nat) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given a value of type t₁ ×' … ×' tᵢ ×' … ×' tₙ, return a value of type tᵢ

Equations

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

def Lean.Meta.PProdN.packLambdas (type : Lean.Expr) (es : Array Lean.Expr) : Lean.MetaM Lean.Expr

Packs multiple type-forming lambda expressions taking the same parameters using PProd.

The parameter type is the common type of the these expressions

For example

packLambdas (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]

will return

fun (n : Nat) => (Nat ×' (Fin n → Fin n))

It is the identity if es.size = 1.

It returns a dummy motive (xs : ) → PUnit or (xs : … ) → True if no expressions are given. (this is the reason we need the expected type in the type parameter).

Equations

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

def Lean.Meta.PProdN.mkLambdas (type : Lean.Expr) (es : Array Lean.Expr) : Lean.MetaM Lean.Expr

The value analogue to PProdN.packLambdas.

It is the identity if es.size = 1.

Equations

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