Counter
Z
- Counter \defs [ n : \nat | n ≥ 0 ]
- Counter::Incr \defs [ ∆Counter, v? : \nat | n′ = n + v? ]
- Counter::Decr \defs [ ∆Counter | n > 0; n′ = n − 1 ]
- Counter::Value \defs [ ΞCounter; v! : \nat | v! = n ]
Bounded counter
- Counter \defs [ n : \nat | n ≥ 0 ]
- Counter::Incr \defs [ ∆Counter, v? : \nat | n′ = n + v? ]
- Counter::Decr \defs [ ∆Counter | n > 0; n′ = n − 1 ]
- Counter::Value \defs [ ΞCounter; v! : \nat | v! = n ]