Lean4
/-- Given `P : ProdTree` representing an iterated product and `e : Expr` which
should correspond to a term of the iterated product, this will return
a list, whose items correspond to the leaves of `P` (i.e. the types appearing in the product),
where each item is the appropriate composition of `Prod.fst` and `Prod.snd` applied to `e`
resulting in an element of the type corresponding to the leaf.
For example, if `P` corresponds to `(X × Y) × Z` and `t : (X × Y) × Z`, then this
should return `[t.fst.fst, t.fst.snd, t.snd]`.
-/
def unpack (t : Expr) : ProdTree → MetaM (List Expr)
| type _ _ => return [t]
| prod fst snd u v => do
let fst' ← fst.unpack <| mkAppN (.const ``Prod.fst [u, v]) #[fst.getType, snd.getType, t]
let snd' ← snd.unpack <| mkAppN (.const ``Prod.snd [u, v]) #[fst.getType, snd.getType, t]
return fst' ++ snd'
