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 : Expr) : MetaM Expr

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

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

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

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

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

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

PProd.fst or And.left (using .proj), inferring the type of e

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

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

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

PProd.snd or And.right (using .proj), inferring the type of e

def Lean.Meta.PProdN.genMk {α : Type} [Inhabited α] (mk : α → α → MetaM α) (xs : Array α) : MetaM α

Essentially a form of foldrM1. Underlies pack and mk, and is useful to construct proofs that should follow the structure of pack and mk (e.g. admissibility proofs)

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

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

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

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

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

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

def Lean.Meta.PProdN.projs (n : Nat) (t e : Expr) : Array Expr

Given a value e of type t = t₁ ×' … ×' tᵢ ×' … ×' tₙ, return the values of type tᵢ

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

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

def Lean.Meta.PProdN.packLambdas (type : Expr) (es : Array Expr) : MetaM 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).

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

The value analogue to PProdN.packLambdas.

It is the identity if es.size = 1.

def Lean.Meta.PProdN.stripProjs (e : Expr) : Expr

Strips topplevel PProd and And projections

def Lean.Meta.PProdN.reduceProjs (e : Expr) : CoreM Expr

Reduces ⟨x,y⟩.1 redexes for PProd and And