Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn_examples 0.2.0
cairn_examples^6 Moves never leave a press in progress
An invariant of cairn_examples 0.2.0.
- Id
cairn_examples^6- Kind
- invariant
- Reads as
- retired
- Version
- 0.2.0
Evidence
retired The runtime owns press tracking; Counter's state no longer has a pressed field, so the invariant was vacuous.
Where it's defined
- Declaration
Examples.Counter.retired_6- Module
Counter- Source
lean/Counter.lean:89atv0.2.0- Statement hash
-
Ledger
cairn_examples^6 is retired in this version's claims.lock. An id never moves or changes meaning.