pairs^1 Pairs window

What it is

The game's window: the pack's name and the counters, the cards in a grid, the field to open a pack from a folder or an https URL, and New Game; when the game is won, the result and New Game in place of the grid.

In this place

Moves

Id	Claim	Reads as
`pairs^2`	Turn a cardClick a face-down card.	proved
`pairs^3`	New GamePress New Game.	proved
`pairs^4`	Open a packType a folder (/… or ~/…) or an https:// URL into the pack field, and press Enter.	proved
`pairs^5`	Cancel loadingWhile a pack is loading, press Cancel.	proved

Flows

Id	Claim	Reads as
`pairs^30`	Find a pairTurn two cards with the same face.	proved
`pairs^31`	A mismatchTurn two cards with different faces.	proved
`pairs^32`	Win a gameTurn the cards of each face in turn, a pair at a time.	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: Pairs.window
Module: Pairs.Claims
Source: lean/Pairs/Claims.lean:43 at v0.1.3
Statement hash: -

Ledger

pairs^1 is active in this version's claims.lock. An id never moves or changes meaning.