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)

Equations

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

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)

Equations

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

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

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

Equations

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

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

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

Equations

• Lean.Meta.mkPProdFstM e = do let __do_lift ← Lean.Meta.inferType e let __do_lift ← Lean.Meta.whnf __do_lift pure (Lean.Meta.mkPProdFst __do_lift e)

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

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

Equations

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

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

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

Equations

• Lean.Meta.mkPProdSndM e = do let __do_lift ← Lean.Meta.inferType e let __do_lift ← Lean.Meta.whnf __do_lift pure (Lean.Meta.mkPProdSnd __do_lift 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)

Equations

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

def Lean.Meta.PProdN.pack (lvl : Level) (xs : Array Expr) : MetaM 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.unpack (e : Expr) (n : Nat) : MetaM (Array Expr)

Unpacks up to n elements from PProd tuple e. Returns fewer if e has < n elements or isn't a PProd. Returns #[] for True/PUnit or when n = 0.

Equations

• Lean.Meta.PProdN.unpack (Lean.Expr.const `True us) n = pure #[]
• Lean.Meta.PProdN.unpack (Lean.Expr.const `PUnit us) n = pure #[]
• Lean.Meta.PProdN.unpack e n = Lean.Meta.PProdN.unpack.go✝ e n #[]

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₃

Equations

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

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ᵢ

Equations

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

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ᵢ

Equations

• Lean.Meta.PProdN.projs n t e = Array.ofFn fun (i : Fin n) => Lean.Meta.PProdN.proj n (↑i) t e

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ᵢ

Equations

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

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

Equations

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

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.

Equations

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

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

Strips top-level PProd and And projections

Equations

• Lean.Meta.PProdN.stripProjs (Lean.Expr.proj `PProd idx e') = Lean.Meta.PProdN.stripProjs e'
• Lean.Meta.PProdN.stripProjs (Lean.Expr.proj `And idx e') = Lean.Meta.PProdN.stripProjs e'
• Lean.Meta.PProdN.stripProjs e = e

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

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

Equations

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