Lean4
/-- This function should act as the "reverse" of `ProdTree.unpack`, constructing
a term of the iterated product out of a list of terms of the types appearing in the product. -/
def pack (ts : List Expr) : ProdTree → MetaM Expr
| type _ _ => do
match ts with
| [] =>
throwError"Can't pack the empty list."
| [a] =>
return a
| _ =>
throwError"Failed due to size mismatch."
| prod fst snd u v => do
let fstSize := fst.size
let sndSize := snd.size
unless ts.length == fstSize + sndSize do
throwError"Failed due to size mismatch."
let tsfst := ts.toArray[:fstSize] |>.toArray.toList
let tssnd := ts.toArray[fstSize:] |>.toArray.toList
let mk : Expr := mkAppN (.const ``Prod.mk [u, v]) #[fst.getType, snd.getType]
return .app (.app mk (← fst.pack tsfst)) (← snd.pack tssnd)
