Lean4
/-- Given two expressions corresponding to iterated products of the same types, associated in
possibly different ways, this constructs the "obvious" function from one to the other. -/
def mkProdFun (a b : Expr) : MetaM Expr := do
let pa ← a.mkProdTree
let pb ← b.mkProdTree
unless pa.components.length == pb.components.length do
throwError "The number of components in{(indentD a)}\nand{indentD b}\nmust match."
for (x, y) in pa.components.zip pb.components do
unless ← isDefEq x y do
throwError "Component{(indentD x)}\nis not definitionally equal to component{indentD y}."
withLocalDeclD `t a fun fvar => do
mkLambdaFVars #[fvar] (← pa.convertTo pb fvar)
