Repository navigation

v2 infer: an integer literal elaborates at an expected type through literal_homomorphism_rows; std.nat Peano row; -1 refused at Nat (XL-2) - #13320

Open

gunbai-bot[bot] wants to merge 105 commits into

mainfrom

session/stern-swift-290-literal

Commits on Oct 4, 2026

v2: bare concat binds the std.algebra collection roster's primitive-call row and is typed by it (WIP)

gunbc-ci-auto-heal
and
claude
committed
6e1c18d
fold_lowering: name the free-monoid carrier on the form (one-variant type does not parse)

gunbc-ci-auto-heal
and
claude
committed
72b9aaa
probe: generic and plain declared callee refusal
gunbc-ci-auto-heal
committed
cbeaffd
v2 infer: a formal containing a type variable inside a constructor is matched and judged (WIP)

gunbc-ci-auto-heal
and
claude
committed
c1ecbe6
generic formal: failure-mode row; warm producers for the controls

gunbc-ci-auto-heal
and
claude
committed
7e4cbc5
floor_pure_producer_share: no annotation inside the roster body

gunbc-ci-auto-heal
and
claude
committed
a326d12
Merge remote-tracking branches 'origin/main' and 'origin/session/stern-swift-290-generic-formal' into session/stern-swift-290
gunbc-ci-auto-heal
committed
b516fb0
concat: failure-mode receipts (third-home disposition, two cost authorities); warm producers; drop probes

gunbc-ci-auto-heal
and
claude
committed
fc5cc26
generic formal: exhaustive arms over node kinds (no closed-coproduct wildcard)

gunbc-ci-auto-heal
and
claude
committed
8ce1880
generic formal: unfold a type alias before comparing constructors; alias controls

gunbc-ci-auto-heal
and
claude
committed
8331557
probe (temporary): where the List alias is indexed
gunbc-ci-auto-heal
committed
21dc371
probe: alias view
gunbc-ci-auto-heal
committed
5ac1713
generic formal: compare the matched formal and the argument with aliases unfolded before the exact judge; drop probe

gunbc-ci-auto-heal
and
claude
committed
8f9d4f7
generic formal: fold (typed) instead of list_map in alias normalization

gunbc-ci-auto-heal
and
claude
committed
eaaad40
stage0: regenerate std_algebra mirror for collection_concat_shape (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
8433728
Merge #13187 branch (alias handling) into concat
gunbc-ci-auto-heal
committed
7d1d264
Merge main into concat (Bool/List de-fork: imports from std.types)

gunbc-ci-auto-heal
and
claude
committed
3cc71fe
Merge remote-tracking branch 'origin/main' into session/stern-swift-290-generic-formal
gunbc-ci-auto-heal
committed
342eaef
Merge main (Bool de-fork: import Bool from std.types)

gunbc-ci-auto-heal
and
claude
committed
9842103
Merge remote-tracking branch 'origin/main' into session/stern-swift-290
gunbc-ci-auto-heal
committed
4fd96b4
Merge remote-tracking branch 'origin/session/stern-swift-290-generic-formal' into session/stern-swift-290
gunbc-ci-auto-heal
committed
7bafdc8
concat roster: exhaustive arms over AlgebraTypeTemplate (no closed-coproduct wildcard)

gunbc-ci-auto-heal
and
claude
committed
ba7f0a3
generic formal: a refined argument matches through its declared carrier (review 75350); refinement and record-wrapper controls

gunbc-ci-auto-heal
and
claude
committed
f4f2b5f
Merge #13187 (refinement carrier, review 75350) into concat
gunbc-ci-auto-heal
committed
3c3ccd7
Merge remote-tracking branch 'origin/main' into session/stern-swift-290
gunbc-ci-auto-heal
committed
7101cbd
concat roster: mint the element binder set with its declared order (type_binder_set_children, required since #13038)

gunbc-ci-auto-heal
and
claude
committed
631cd76
one alias rule: transparent aliases normalized by the obligation producer for both routes; refinements never unfold; generic shortcut and alias arms deleted (review 75435)

gunbc-ci-auto-heal
and
claude
committed
9e73727
one obligation constructor: declared, produced and refinement carrier all alias-normalized at every infer obligation

gunbc-ci-auto-heal
and
claude
committed
764dc9d
generic formal: the refinement carrier is matched alias-normalized, like the formal

gunbc-ci-auto-heal
and
claude
committed
ba7a8d3
Merge #13187 (one alias rule, review 75435)
gunbc-ci-auto-heal
committed
194950b
fold_lowering: match the roster form directly at each reader; delete the Bool predicate (review 75785)

gunbc-ci-auto-heal
and
claude
committed
f02888e
Merge remote-tracking branch 'origin/main' into session/stern-swift-290
gunbc-ci-auto-heal
committed
83f02ef
concat roster: plain binder set again after #13038's revert (#13293); the declared-order mint returns with #13038

gunbc-ci-auto-heal
and
claude
committed
eddcb4c
Merge remote-tracking branch 'origin/main' into session/stern-swift-290-count
gunbc-ci-auto-heal
committed
5db6319
v2: bare count binds the std.algebra collection size row, a stated Int (declared departure, literal-elaboration trigger)

gunbc-ci-auto-heal
and
claude
committed
c80f0b7
stage0: regenerate std_algebra mirror for collection_count_shape (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
39d7cce
v2 infer: an integer literal elaborates at an expected type through literal_homomorphism_rows; std.nat Peano row; count's row back to Nat (WIP)

gunbc-ci-auto-heal
and
claude
committed
2c6385f
probe (temporary)
gunbc-ci-auto-heal
committed
9972b87
probe 2
gunbc-ci-auto-heal
committed
b0953af
probe 3
gunbc-ci-auto-heal
committed
e1cbd84
literal elaboration: negated literal refuses at a row-backed destination; operator reader dropped (no observable consumer); controls: two-outcome eval, Nat count fixtures with a std.nat peer

gunbc-ci-auto-heal
and
claude
committed
1dfaf23
probe (temporary)
gunbc-ci-auto-heal
committed
40bca64
Merge main (#13187 landed) into #13207
gunbc-ci-auto-heal
committed
0e22f66
Merge #13207 (main with #13187) into count
gunbc-ci-auto-heal
committed
2abcaea
literal elaboration: count stays the judged stated Int (calm-boar-904 option B); departure trigger gains the declared-return condition; count files restored to #13307's

gunbc-ci-auto-heal
and
claude
committed
04935d1
Merge #13307 head
gunbc-ci-auto-heal
committed
f652512
concat controls: one real-path claim plus supplied-input signature claims (DESIGN 3 witness rule); warm rows dropped (tightened freeze)

gunbc-ci-auto-heal
and
claude
committed
206562f
stage0: regenerate mirrors for the std.nat literal row and the fork note (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
3cba1a7
Merge #13207 (restructured)
gunbc-ci-auto-heal
committed
8f623ac
count controls: one real-path claim plus supplied-input signature claims (DESIGN 3); warm rows dropped

gunbc-ci-auto-heal
and
claude
committed
6ec296b
roster: drop the cca rows a merge resurrected
gunbc-ci-auto-heal
committed
34e005d
count controls: typed helper for the formal's kind
gunbc-ci-auto-heal
committed
daf4fa7
literal controls: one real-path claim plus supplied-input claims at infer_literal_elaborates_at (DESIGN 3); warm rows dropped

gunbc-ci-auto-heal
and
claude
committed
6c67fd7
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into session/stern-swift-290-literal
gunbc-ci-auto-heal
committed
a2485f0

Commits on Oct 5, 2026

Merge main (#13043 landed); collection_concat_realization's one real-path claim as single-claim fill debt (sharp-raven-357)

gunbc-ci-auto-heal
and
claude
committed
8f251a0
Merge remote-tracking branch 'origin/session/stern-swift-290' into session/stern-swift-290-count
gunbc-ci-auto-heal
committed
4a10199
Merge #13207 (#13043 landed); collection_count_realization's one real-path claim as single-claim fill debt

gunbc-ci-auto-heal
and
claude
committed
91757f6
Merge #13307 (#13043 landed); literal_elaboration's one real-path claim as single-claim fill debt

gunbc-ci-auto-heal
and
claude
committed
2f8b765
fill debt: cite #13307's actual floor run (37240332005)
gunbc-ci-auto-heal
committed
ac5f03b
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into session/stern-swift-290-literal
gunbc-ci-auto-heal
committed
6461dfe
fill debt: provenance above the declaration, not inside the list body (annotations are module-item grain)
gunbc-ci-auto-heal
committed
61bc6d8
fill debt: provenance above the declaration, not inside the list body (annotations are module-item grain)
gunbc-ci-auto-heal
committed
7deab30
fill debt: provenance above the declaration, not inside the list body (annotations are module-item grain)
gunbc-ci-auto-heal
committed
dd2ee27
count's stated-Int result as a typed gunbc.rung_drop row (reviews 76222, 76223); fork note points to it

gunbc-ci-auto-heal
and
claude
committed
f40abad
infer: a roster row whose signature cannot be read refuses, located -- the lookup is three-way and never falls through to the row's template value (review 76235)

gunbc-ci-auto-heal
and
claude
committed
8952e50
roster lookup over a supplied roster and infer's roster arm as its own function, so the unreadable-row refusal RED is authorable and fires at infer (review 76235)

gunbc-ci-auto-heal
and
claude
committed
3ce4c22
fold_lowering: the boundary reversal points to its recorded receipt, not a message handle (review 76242)

gunbc-ci-auto-heal
and
claude
committed
c51e190
stage0: regenerate gunbc_structural_realization_bindings mirror against the merged tree (bootstrap from #13307's head; fixed point at round 1)

gunbc-ci-auto-heal
and
claude
committed
0d60fa4
regenerate docs/design-rung-drops.md and the std_algebra mirror for the count drop row (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
d788183
Merge #13207 (review 76235 and 76242 fixes) into #13307
gunbc-ci-auto-heal
committed
7269202
Merge #13307 (typed count drop row; review 76255) into #13320

gunbc-ci-auto-heal
and
claude
committed
619a589
fork note: the type-disagreement pointer is a // annotation, not appended string data; the count drop's population lists the seed's method-typing path (review 76274)

gunbc-ci-auto-heal
and
claude
committed
0b7280b
regenerate drop docs and std_algebra mirror (note annotation; seed path in population)

gunbc-ci-auto-heal
and
claude
committed
5ca4c76
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into session/stern-swift-290-literal
gunbc-ci-auto-heal
committed
e1b7f02
concat controls: the synthetic unreadable row cites a declaration that exists (its own producer), not an absent std.algebra member (declarations phase)

gunbc-ci-auto-heal
and
claude
committed
a8dcd1d
Merge remote-tracking branch 'origin/session/stern-swift-290' into session/stern-swift-290-count
gunbc-ci-auto-heal
committed
7f54451
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into session/stern-swift-290-literal
gunbc-ci-auto-heal
committed
45851ca
literal elaboration: the table's refusal carries its own typed reason (HomomorphismDuplicated), not a generic one (review 76326)

gunbc-ci-auto-heal
and
claude
committed
447aaa7
count drop: the shape comment points to the drop row; the population is stated structurally, not as a transcribed scan figure (review 76335)

gunbc-ci-auto-heal
and
claude
committed
8a01c36
regenerate drop docs for the structural population (review 76335)

gunbc-ci-auto-heal
and
claude
committed
f908e4f
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into session/stern-swift-290-literal
gunbc-ci-auto-heal
committed
a51116c
Merge main (#13207 landed) into count; mirror and drop docs to be regenerated

gunbc-ci-auto-heal
and
claude
committed
515bd86
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into session/stern-swift-290-literal
gunbc-ci-auto-heal
committed
58f5117
regenerate std_algebra mirror and drop docs against the merged tree (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
871d8d4
regenerate std_algebra mirror and drop docs against the merged tree (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
e2f8a63
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into session/stern-swift-290-literal
gunbc-ci-auto-heal
committed
f444f57

Commits on Oct 6, 2026

Merge main into #13307 (rung-drop roster now derived; mirror and drop docs to be regenerated)

gunbc-ci-auto-heal
and
claude
committed
3da80aa
count test: the subject comment points at the departure's authority, the rung_drop row (review 76865)

gunbc-ci-auto-heal
and
claude
committed
1a07969
Regenerate std_algebra mirror and drop docs against the merged tree (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
1994555
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into HEAD
gunbc-ci-auto-heal
committed
5f05060
Merge remote-tracking branch 'origin/main' into HEAD
gunbc-ci-auto-heal
committed
744d6a4
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into HEAD
gunbc-ci-auto-heal
committed
d593c7a
Merge main into #13307 (#13388's optional re-home; generated files to be regenerated)

gunbc-ci-auto-heal
and
claude
committed
192306b
Repoint #13307's v2.std.optional import to std.optional (tools.source_reference_repoint) and regenerate the std_algebra mirror and drop docs (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
46f5a8d
Merge #13307 (main + #13388 re-home) into #13320; generated mirror to be regenerated

gunbc-ci-auto-heal
and
claude
committed
8df1088
Merge remote-tracking branch 'origin/main' into HEAD
gunbc-ci-auto-heal
committed
d8f8483
Repoint #13320's v2.std.optional import to std.optional (tools.source_reference_repoint) and regenerate the structural_realization_bindings mirror (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
037a051
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into HEAD
gunbc-ci-auto-heal
committed
d074251
Comments: count's result is not uniformly Nat -- the free monoid's count states Int under its declared drop (review 77155)

gunbc-ci-auto-heal
and
claude
committed
216c6f2
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into HEAD
gunbc-ci-auto-heal
committed
1ad2232
Merge remote-tracking branch 'origin/main' into HEAD
gunbc-ci-auto-heal
committed
981392b
Regenerate docs/design-rung-drops.md against main + #13490 (adds this PR's count drop)

gunbc-ci-auto-heal
and
claude
committed
e8be9d2
Merge remote-tracking branch 'origin/session/stern-swift-290-count' into HEAD
gunbc-ci-auto-heal
committed
bc59995
Nat elaborates a literal through its kernel grounding and declared range, not a Peano homomorphism row (calm-boar-904 ruling A, review 77219)

gunbc-ci-auto-heal
and
claude
committed
24924d5
Regenerate the literal_elaboration and structural_realization_bindings mirrors (fixed point at round 2)

gunbc-ci-auto-heal
and
claude
committed
d974378