Mathematics · proofs · software

Proof Path Theory · Lean source

WrongDecoder.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/WrongDecoder.lean3 lines

Original source pathformal/negative_controls/WrongDecoder.lean

Skip source text

1 import ProofPath.Recovery
2 -- The proposed decoder forgets the Boolean answer and is wrong at true.
3 example : (fun _ : Unit => false) () = true := by decide

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: dbcc5e9c20f64c49b6d5ea4e006b4642f69834280dbd60a3021d46c6b520981a

Original source on GitHub

Back to Proof Path Theory