Cairn
Docs
Claims
Blog
Packages
Claim ยท sky 0.3.1
sky^1 Sky window
A place of sky 0.3.1.
- Id
sky^1- Kind
- place
- Reads as
- no proof
- Version
- 0.3.1
What it is
Sky's window. Signed out, the sign-in screen: handle or email, app password, service, Sign in, and what went wrong. Signed in: the home feed (Following), with Refresh and Account above it and a status line that offers new posts.
In this place
Moves
| Id | Claim | Reads as |
|---|---|---|
sky^4 | RefreshWhile signed in, press Refresh. | proved |
sky^6 | Type your handle or emailWhile signed out, type in the Handle or email field, and press Enter. | proved |
sky^7 | Type your app passwordWhile signed out, type in the App password field, and press Enter. | proved |
sky^8 | Type the serviceWhile signed out, type in the Service field (empty: https://bsky.social, or the default Sky reads at launch). | proved |
sky^9 | What's an app password?While signed out, press What's an app password? | proved |
sky^10 | Sign inType a handle or email and an app password, and press Sign in. It is enabled exactly when both fields are typed in and no sign-in (or resume) is in flight. | proved |
sky^11 | Sign outWhile signed in, open the account panel and press Sign out. | proved |
sky^12 | Cancel signing inWhile Sky has been signing in or resuming the session for a few seconds, press Cancel. | proved |
sky^13 | AccountWhile signed in, press Account (Done when it is open). | proved |
sky^33 | Show new postsAfter a refresh put posts above the one you are reading, press N new posts. | 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:50atv0.3.1- Statement hash
-
Ledger
sky^1 is active in this version's claims.lock. An id never moves or changes meaning.