Cairn Docs Claims Blog Packages

Claim · cairn 0.2.3

cairn^6 Moves never leave a press in progress

An invariant of cairn 0.2.3.

Id: cairn^6
Kind: invariant
Reads as: retired
Version: 0.2.3

All of cairn 0.2.3's claims

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: Examples.Counter
Source: lean/Examples/Counter.lean:92 at v0.2.3
Statement hash: -

Ledger

cairn^6 is retired in this version's claims.lock, statement 5de1d6cd863262b8. An id never moves or changes meaning.