proof/progress · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof progress

20 files

gildrb.com · progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call) · 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/

child_loop_is_a_stall.bend

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

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

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

goal_compared_check.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

goal_entry_answers.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

goal_entry_example.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

goal_entry_malformed_exact.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

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

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

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

goal_judge_exact.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

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

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

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

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

goal_req_fits_example.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

goal_stopped_exact.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

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

work_counts_distinct.bend

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)