Claim · sky 0.3.1
sky^30 Reach the end of the feed
A move of sky 0.3.1, in The feed.
What you do
Scroll the feed to its end, while it isn't at the end of the timeline.
What you see
Loading… shows at the end, and the next page, from the cursor the feed holds, is appended below the posts already there; if a refresh replaced the feed first, the page is dropped.
Evidence
| proved | sound appear | Sky.reachEnd.appear.sound |
| fuzzed | Not shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95). | |
| tested | Not shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95). | |
| seen | Not shown yet: a screenshot of the app shows it. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Sky.reachEnd- Module
Sky.Claims- Source
lean/Sky/Claims.lean:154atv0.3.1- Statement
Sky.reachEnd.enabledSky.reachEnd.appear.post- Statement hash
c248dc5bd68f349a
Ledger
sky^30 is active in this version's claims.lock, statement c248dc5bd68f349a. An id never moves or changes meaning.