Lean4
/-- `additivizeLemmas names argInfo desc t` runs `t` on all elements of `names`
and adds translations between the generated lemmas (the output of `t`).
`names` must be non-empty. -/
def additivizeLemmas {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT CoreM m] (names : Array Name)
(argInfo : ArgInfo) (desc : String) (t : Name → m (Array Name)) : m Unit := do
let auxLemmas ← names.mapM t
let nLemmas := auxLemmas[0]!.size
for (nm, lemmas) in names.zip auxLemmas do
unless lemmas.size == nLemmas do
throwError "{names[0]!} and {nm } do not generate the same number of {desc}."
for (srcLemmas, tgtLemmas) in auxLemmas.zip <| auxLemmas.eraseIdx! 0do
for (srcLemma, tgtLemma) in srcLemmas.zip tgtLemmas do
insertTranslationAndInfo srcLemma tgtLemma argInfo
