pairs^4 Open a pack

What you do

Type a folder (/… or ~/…) or an https:// URL into the pack field, and press Enter.

What you see

The text appears in the field. On Enter, the pack starts loading beside the game, and any pack still loading stops; the game goes on until every image of the new pack has loaded, then a new game of it is dealt. A path or URL that can't be used, a pack.json that doesn't parse, or an image that fails says what went wrong and leaves the game as it was.

Evidence

proved	sound edit	`Pairs.packField.edit.sound`
proved	sound submit	`Pairs.packField.submit.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: Pairs.packField
Module: Pairs.Claims
Source: lean/Pairs/Claims.lean:99 at v0.1.3
Statement: Pairs.packField.edit.post Pairs.packField.submit.post
Statement hash: 87dd291de3bcc780

Ledger

pairs^4 is active in this version's claims.lock, statement 87dd291de3bcc780. An id never moves or changes meaning.