Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^212 Counter and ids

An invariant of cairn_examples 0.2.0.

Id
cairn_examples^212
Kind
invariant
Reads as
proved
Version
0.2.0

All of cairn_examples 0.2.0's claims

What it says

The counter shows the number of active todos, over all todos; todo ids are distinct, in every reachable state. (T24, T34)

Evidence

provedinitExamples.Todo.counterAndIds.init
provedstepExamples.Todo.counterAndIds.step
provedreceiveExamples.Todo.counterAndIds.receive
provedreachableExamples.Todo.counterAndIds.reachable
provedreachableAllExamples.Todo.counterAndIds.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.Todo.counterAndIds
Module
Todo
Source
lean/Todo.lean:183 at v0.2.0
Machine
Examples.Todo.machine
Statement
Examples.Todo.counterAndIds.holds
Statement hash
8b1d23f718f063ec

Ledger

cairn_examples^212 is active in this version's claims.lock, statement 8b1d23f718f063ec. An id never moves or changes meaning.