proof/command · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof command

23 files

at bend/all-shell

gildrb.com · 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/ · 2w ago

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/

command_enter_on_row.bend

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

command_enter_without_row.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>

command_ffi_answers.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>

command_ffi_left_over.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>

command_ffi_malformed.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>

command_ffi_menu_round_trip.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/

command_ffi_out_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

command_ffi_res_round_trip.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/

command_ffi_round_trip.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/

command_ffi_witness.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>

command_free_takes_rest.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/

command_memory_model_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>

command_memory_model_keys_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>

command_menu_lists_children.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/

command_menu_names_first_word.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/

command_menu_shut_off_path.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/

command_path_runs_itself.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/

command_stale_row_ignored.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>

command_stray_is_not_a_command.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/

command_tab_completes_row.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>

command_tab_without_row.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>

command_unknown_runs_nothing.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/