pub fn generate(ctx: &mut Context, name: &str)Expand description
Generate and REGISTER the equation lemmas a definition owes.
Every candidate goes through inference and the checked declaration gateway. Failed optional candidates are omitted; they cannot poison a valid source declaration or enter the pending-obligation/refusal ledger. Existing names, including pending user definitions, are reserved. Successful lemmas share the existing auxiliary ownership bookkeeping so source replacement invalidates them.