pub fn foreign_axiom_note(name: &str) -> Option<&'static str>Expand description
The diagnostic sentence for a constant the trusted base deliberately lacks, or None when the
name is simply not registered (a typo, a missing import, an out-of-scope local).
A kernel that answers UnboundVariable("sorryAx") invites exactly one repair — add the name to
the prelude — and that repair is catastrophic. A kernel that answers UnboundVariable("id")
invites the right one. Same arm, same shape, different name: this function is the only thing
that can tell them apart.