proof/wire · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof wire

1 folder · 43 files

gildrb.com · wire: pin every numeric writer and reader to an independent decimal spec · 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_reads_spelled.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_bool_spelled.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_reads_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

wire_nats_reads_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_str_reads_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

wire_strs_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_reads_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

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_reads_decimal.bend

wire: pin every numeric writer and reader to an independent decimal spec

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