pub fn derive_auxiliaries(ctx: &Context, ind: &str) -> Vec<DerivedAux>Expand description
Everything the declaration of ind should bring with it, in DEPENDENCY ORDER, for a
caller to register verbatim:
for aux in derive_auxiliaries(&ctx, name) {
ctx.add_definition(aux.name, aux.ty, aux.term);
}The list is BEST-EFFORT: an auxiliary that this kernel genuinely cannot state for this
inductive (an indexed family with no index unifier, a Prop where disjointness is a
category error, a carrier above Type 0 where Eq cannot even be applied) is OMITTED
rather than faked. Registration is therefore never blocked by a shape we do not reach, and
what IS returned was type-checked. Call the individual derive_* functions when you want
the REASON one is missing — each returns a CertificationError naming it.
It also never DISPLACES: a name already in ctx is left alone. Registration overwrites, so
without this the umbrella run over a prelude type would silently replace the hand-written,
separately-tested decEqNat with a freshly derived one — same intent, different term, and
nothing would have reported the swap.