Cairn Docs Claims Blog Packages

Claim ยท cairn 0.2.1

cairn^460 At most five recent items

An invariant of cairn 0.2.1.

Id
cairn^460
Kind
invariant
Reads as
proved
Version
0.2.1

All of cairn 0.2.1's claims

What it says

Recent Items never lists more than five items, however many are added.

Evidence

provedinitExamples.Tray.fewRecent.init
provedstepExamples.Tray.fewRecent.step
provedreceiveExamples.Tray.fewRecent.receive
provedreachableExamples.Tray.fewRecent.reachable
provedreachableAllExamples.Tray.fewRecent.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Examples.Tray.fewRecent
Module
Examples.Tray
Source
lean/Examples/Tray.lean:161 at v0.2.1
Machine
Examples.Tray.machine
Statement
Examples.Tray.fewRecent.holds
Statement hash
766546c5055d42df

Ledger

cairn^460 is active in this version's claims.lock, statement 766546c5055d42df. An id never moves or changes meaning.