Lean4
/-- Run applyReplacementFun on the given `srcDecl` to make a new declaration with name `tgt` -/
def updateDecl (tgt : Name) (srcDecl : ConstantInfo) (reorder : List (List Nat)) (dont : List Ident) :
MetaM ConstantInfo := do
let mut decl := srcDecl.updateName tgt
if 0 ∈ reorder.flatten then
decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
let dont ← getDontTranslates dont srcDecl.type
decl := decl.updateType <| ← reorderForall reorder <| ← applyReplacementForall dont <| renameBinderNames decl.type
if let some v := decl.value? then
decl := decl.updateValue <| ← reorderLambda reorder <| ← applyReplacementLambda dont v
else if let .opaqueInfo info := decl then -- not covered by `value?`
decl := .opaqueInfo { info with value := ← reorderLambda reorder <| ← applyReplacementLambda dont info.value }
return decl
