pub const FOREIGN_AXIOMS: &[(&str, &str)];Expand description
Axioms and constants LOGOS deliberately does NOT have, each with the sentence a diagnostic should say instead of “unbound variable”.
This exists because the information that distinguishes sorryAx from a typo is the NAME and
nothing else: inside infer_type an unregistered Term::Global carries no provenance, so a
single verdict for the whole arm cannot both say “your proof rests on an admission” for
sorryAx and “this local is out of scope” for id. A name-keyed registry separates them, and
putting it HERE — beside the trusted base it is the complement of — is what keeps the two in
step: an axiom that later gets registered must be deleted from this table, and
the_foreign_axiom_registry_is_disjoint_from_the_trusted_base in the lane’s own test file
fails if it is not.