Skip to content

Commit 398287e

Browse files
tcoratgerclaude
andauthored
refactor(timeline): name the within-slot interval and drop redundant wrap (#1133)
The within-slot interval position was wrapped in an Interval only to be unwrapped one line later in the match via int(...). Compute the plain int once and match on it directly. Rename it from a vague absolute-interval name to one that says it is the position within the slot. Behavior is identical; just check passes. Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 8cf92a4 commit 398287e

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

src/lean_spec/spec/forks/lstar/timeline.py

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,10 @@ def tick_interval(
2121
) -> tuple[LstarStore, list[SignedAggregatedAttestation]]:
2222
"""Advance store time by one interval and perform interval-specific actions."""
2323
store = store.model_copy(update={"time": store.time + Interval(1)})
24-
current_interval = Interval(int(store.time) % int(INTERVALS_PER_SLOT))
24+
interval_within_slot = int(store.time) % int(INTERVALS_PER_SLOT)
2525
new_aggregates: list[SignedAggregatedAttestation] = []
2626

27-
match int(current_interval):
27+
match interval_within_slot:
2828
# Slot start: ingest pending attestations once the slot's proposal lands.
2929
case 0 if has_proposal:
3030
store = self.accept_new_attestations(store)

0 commit comments

Comments
 (0)