Claim ยท sky 0.1.0
sky^1 Sky window
A place of sky 0.1.0.
- Id
sky^1- Kind
- place
- Reads as
- no proof
- Version
- 0.1.0
What it is
Sky's window. Bare for now: who is signed in, what went wrong, a button for each thing you can do, and the first posts of the home feed.
In this place
Moves
| Id | Claim | Reads as |
|---|---|---|
sky^2 | Sign inWhile signed out, press Sign in (with the service, handle and app password typed). | proved |
sky^3 | Load moreWith a feed that isn't at its end, press Load more. | proved |
sky^4 | RefreshWhile signed in, press Refresh. | proved |
sky^5 | Sign outWhile signed in or signing in, press Sign out. | proved |
Evidence
| no proof | A place states where claims live; it has nothing to prove. | |
| seen | Not shown yet: a screenshot of the app shows it. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Sky.window- Module
Sky.Claims- Source
lean/Sky/Claims.lean:30atv0.1.0- Statement hash
-
Ledger
sky^1 is active in this version's claims.lock. An id never moves or changes meaning.