Skip to main content

AXIOM_WHITELIST

Constant AXIOM_WHITELIST 

Source
pub const AXIOM_WHITELIST: [&str; 3];
Expand description

Axioms a certified proof may depend on without weakening trust.

These are Lean’s standard classical foundations. Anything else (notably sorryAx) means the proof is not the proof we asked for.