proof/wire · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof wire

1 folder · 32 files

at bend/stackfix

gildrb.com · laws: a Nat on the wire is its decimal digits (every entry); the command reply readers read the spelled reply grammar; every command answer but the malformed error comes from an input that begins with a request · 2w ago

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_bool_exact.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_bool_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_bool_not_err.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_bool_round_trip.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_digits_spells.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_end_exact.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_err_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_list_exact.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_list_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_nat_decimal.bend

laws: a Nat on the wire is its decimal digits (every entry); the command reply readers read the spelled reply grammar; every command answer but the malformed error comes from an input that begins with a request

wire_nat_decoded_fits.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_nat_exact.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_nat_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_nat_leading_zero_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_nat_not_err.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_nat_too_long.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_nat_unterminated_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_nat_zero_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_nats_spells.bend

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

wire_str_decoded_fits.bend

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

wire_str_exact.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_str_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_strs_decoded_fit.bend

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

wire_strs_exact.bend

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

wire_strs_example.bend

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

wire_strs_round_trip.bend

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

wire_strs_spells.bend

command entry laws: spelled with spec spellers over the W. primitives (the circular command_ffi_answers no longer the only link to the model); decoders exact; spacing and stale-row arms pinned; spellers shared in laws/base.bend

wire_too_long_exists.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

wire_u32_exact.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_u32_example.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

wire_u32_round_trip.bend

proofs: files past 1,000 lines become folders by topic (proof/base/, proof/<area>/base/, proof/optchat/push_agrees_always/); P1 binders renamed