Proof Path Theory · Lean source

ExtraAxiom.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Local imports (1)

negative_controls/ExtraAxiom.lean6 lines

Original source path

formal/negative_controls/ExtraAxiom.lean

Skip declarations and read code

1 import ProofPath.Field
2 namespace ExtraAxiom
3 axiom assumedFalse : False
4 theorem invalid : False := assumedFalse
5 end ExtraAxiom
6 #print axioms ExtraAxiom.invalid

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 5b6efa11f42cb6955972e1d4642b840e05d95740455844a84f65cb6016dc9d00

Original source on GitHub

Back to Proof Path Theory