Lean4
/-- Reorder lambda-binders. See doc of `reorderAttr` for the interpretation of the argument -/
def reorderLambda (reorder : List (List Nat)) (src : Expr) : MetaM Expr := do
if let some maxReorder := reorder.flatten.max? then
let maxReorder := maxReorder + 1
lambdaBoundedTelescope src maxReorder fun xs e => do
if xs.size = maxReorder then
mkLambdaFVars (xs.permute! reorder) e
else
-- we don't have to consider the case where the given permutation is out of bounds,
-- since `reorderForall` applied to the type would already have failed in that case.
forallBoundedTelescope (← inferType e) (maxReorder - xs.size) fun ys _ => do
mkLambdaFVars ((xs ++ ys).permute! reorder) (mkAppN e ys)
else
return src
