Skip to content

Commit 9b8695d

Browse files
committed
Delete duplicate broken orphan modules
These three modules were committed in 8b8fc03 ("further proofing bridges") but never compiled and duplicated functionality already covered by in-suite modules: * EchoCategory.agda (58 sigs, 0 data) — duplicate of EchoCategorical.agda; had self-shadowing `_→_` and `_∘_` definitions that parse-errored. * EchoCNO.agda (8 sigs) — duplicate of EchoCNOBridge.agda; used invalid `Σ (x : A) (λ _ → ...)` binder syntax and had a dangling top-level `where` clause. * EchoJanusSimple.agda (9 sigs) — duplicate of EchoJanusBridge.agda; same invalid `Σ (x : A) (...)` binder syntax. Nothing in the verified suite (All.agda) imported any of them. Deleting them removes silently-broken Agda from the tree without changing what compiles. https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK
1 parent 8b8fc03 commit 9b8695d

3 files changed

Lines changed: 0 additions & 441 deletions

File tree

proofs/agda/EchoCNO.agda

Lines changed: 0 additions & 66 deletions
This file was deleted.

proofs/agda/EchoCategory.agda

Lines changed: 0 additions & 323 deletions
This file was deleted.

0 commit comments

Comments
 (0)