Lean4
/-- Add the structure fields of `src` to the translations dictionary
so that future uses of `to_additive` will map them to the corresponding `tgt` fields. -/
def proceedFields (src tgt : Name) (argInfo : ArgInfo) : CoreM Unit := do
let env ← getEnv
let aux := proceedFieldsAux src tgt argInfo
aux fun declName ↦
if isStructure env declName then
let info := getStructureInfo env declName
Array.ofFn (n := info.fieldNames.size) (info.getProjFn? · |>.get!)
else
#[]
-- add translations for the automatically generated instances with `extend`.
aux fun declName ↦
if isStructure env declName then
getStructureInfo env declName |>.parentInfo |>.filterMap fun c ↦ if !c.subobject then c.projFn else none
else
#[]
-- add translations for the constructors of an inductive type
aux fun declName ↦
match env.find? declName with
| some (ConstantInfo.inductInfo { ctors, .. }) => ctors.toArray
| _ => #[]
