Skip to content

Commit 7a4a72a

Browse files
sync(cartridges/007-mcp): BindAddress.proof → .witness (closes #32) (#33)
Cartridge sync from \`boj-server-cartridges#34\` (merged 2026-06-02 13:12Z). \`proof\` is a reserved keyword in Idris2 0.8.0; cannot be a record field. Two-line rename: field declaration + one call site. ## Refs - boj-server-cartridges#34 (canonical) - valence-shell#112 (precedent + symptom report) - Memory: reference_idris2_0_8_0_reserved_keywords.md Closes #32. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent d7f6f30 commit 7a4a72a

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

cartridges/007-mcp/abi/Oo7Mcp/SafeCli.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ record BindAddress where
4646
constructor MkBindAddress
4747
host : String
4848
port : Int
49-
proof : IsLoopback
49+
witness : IsLoopback
5050

5151
||| The one and only production bind — 127.0.0.1:1066.
5252
||| Port 1066 chosen in design-log decision-log 2026-04-20.
@@ -68,7 +68,7 @@ oo7_mcp_bind_port = cartridgeBind.port
6868
||| Lets the adapter sanity-check that the proof travelled across FFI.
6969
export
7070
oo7_mcp_bind_family : Int
71-
oo7_mcp_bind_family = case cartridgeBind.proof of
71+
oo7_mcp_bind_family = case cartridgeBind.witness of
7272
Ipv4Loopback => 4
7373
Ipv6Loopback => 6
7474

0 commit comments

Comments
 (0)