pub const ADMITTED_AXIOMS: &[&str];Expand description
Names that mark a proof as ADMITTED rather than proved.
sorryAx is Lean’s; the rest are the other placeholders a translated or hand-edited
environment can acquire. LOGOS deliberately registers NONE of them, so seeing one means a
caller reached past StandardLibrary::register — which is the single most dangerous thing that
can happen to a proof library, because the result type-checks, BOTH kernels agree, and
verified == true really does hold.