proof/theme · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof theme

1 folder · 52 files

gildrb.com · spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel) · 1w ago

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

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/

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

theme_builtin_before_custom_example.bend

theme, color: run as compiled Bend (entries ffi_theme 62, ffi_color 67); the Rust copies, the bridge and the law-covered tests go

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

theme_chase_rule.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_concrete_spec.bend

laws: theme and color helpers pinned to specs (a fresh adversary's prefix name, ignored background, constant mode, vacuous legibility, loose hex digits)

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

theme_entry_color.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_entry_invalid.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

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

theme_ffi_answers.bend

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

theme_ffi_example.bend

theme, color: run as compiled Bend (entries ffi_theme 62, ffi_color 67); the Rust copies, the bridge and the law-covered tests go

theme_ffi_left_over.bend

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

theme_ffi_malformed_exact.bend

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

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

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

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

theme_fill_required.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_hit_spec.bend

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

theme_legible_spec.bend

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

theme_light_example.bend

laws: theme and color helpers pinned to specs (a fresh adversary's prefix name, ignored background, constant mode, vacuous legibility, loose hex digits)

theme_light_spec.bend

laws: theme and color helpers pinned to specs (a fresh adversary's prefix name, ignored background, constant mode, vacuous legibility, loose hex digits)

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

theme_mode_background.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_mode_name_free.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_palette_name_free.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

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

theme_parse_painted.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_parse_rejected.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_pick_broken.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_pick_cause.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_pick_clashes.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

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

theme_pick_quiet.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_pick_res.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_prefix_example.bend

laws: theme and color helpers pinned to specs (a fresh adversary's prefix name, ignored background, constant mode, vacuous legibility, loose hex digits)

theme_read_card.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_read_first_error.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_read_info.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_read_loaded.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_read_missing.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_read_page.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

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

theme_resolve_empty.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_resolve_first.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_resolve_missing.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_shipped_legible.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_shipped_status_distinct.bend

bend: run.bend, optchat.bend, theme.bend past 1,000 lines become folders, one module per responsibility

theme_sources_order.bend

theme, color: run as compiled Bend (entries ffi_theme 62, ffi_color 67); the Rust copies, the bridge and the law-covered tests go

theme_status_distinct_spec.bend

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

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

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