Cairn · module
Cairn.Claim
lean/Cairn/Claim.lean
Claims: statements about the product with durable ids.
The vocabulary is fixed here; the move, flow, invariant, assume and place commands
that create claims, and the ledger that guards their ids, live in Cairn.Claims.
Order
Structures 2
ClaimInfo : Type
The human half of a claim: what a reviewer reads next to the formal statement.
ControlRef : Type
One instance of a move's control on screen. A move like "toggle a todo" has one control
per todo; key tells them apart (0 when there is only one). Shown as ^5 or ^5#12.
Fields
claim : ClaimId
key : NatInductive types 1
ClaimKind : Type
Definitions 2
ClaimId : Type
A claim id, written ^N. Never renumbered, reused or deleted.
label (c : ControlRef) : String
How a control is written in ids and on the map's pins: ^5, or ^5#12 for a keyed one.
example : ({ claim := 5 } : ControlRef).label = "^5" := by decide
example : ({ claim := 5, key := 12 } : ControlRef).label = "^5#12" := by decide
Instances 9
instDecidableEqClaimKind : DecidableEq ClaimKind
instInhabitedClaimKind : Inhabited ClaimKind
instReprClaimKind : Repr ClaimKind
instInhabitedClaimInfo : Inhabited ClaimInfo
instReprClaimInfo : Repr ClaimInfo
instDecidableEqControlRef : DecidableEq ControlRef
instHashableControlRef : Hashable ControlRef
instReprControlRef : Repr ControlRef
instInhabitedControlRef : Inhabited ControlRef