Proof Path Theory · Lean source
MergedContext.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/MergedContext.lean11 lines
Original source path
formal/negative_controls/MergedContext.lean1 import ProofPath.ExtensionExamples
2 -- This is exactly the false negative-observation conjunct of the proposed
3 -- merged realization. Unfolding the contract is not itself a test failure.
4 example : ProofPath.ExtensionExamples.target.Extends ({()} : Set Unit) {()}
5 (fun _ => True) := by
6 refine ⟨?_, ?_, ?_⟩
7 · exact ⟨by intro v h; exact False.elim h, by intro j; exact Empty.elim j⟩
8 · intro _ _; trivial
9 · intro v hv
10 change ¬ True
11 decide
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: dc3f7b14656233e9b7a3bc4146de5a79870b49cd4334beed01290c40a9dbc26a