Natural numbers
NAT types are natural numbers. You can start at 0 using,
Zero
and have a way to get the next one, i.e. its successor using,
Succ
Nat is used as a part of folding.
scilla_version 0(***************************************************)(* The built-in ADT "Nat" *)(***************************************************)import NatUtils
contract NatType()
field counter: Nat = Zero
(* emit the current value of the counter in an event *)procedure EmitCounterAsNumber() c <- counter; number = nat_to_int c; (* from NatUtils *) ev = {_eventname : "EmitCounter"; counter_value: number}; event evend
(* Increase the counter: get next Peano Number *)transition Increase() c <- counter; next = Succ c; counter := next; EmitCounterAsNumberend
(* Decrease the counter: get previous Peano Number *)(* floored at Zero, i.e. there is no previous to Zero *)transition DecreaseFlooredAtZeo() c <- counter; previous_opt = nat_prev c; (* from NatUtils *) previous = let p = match previous_opt with | None => (* counter was Zero, remains at Zero *) Zero | Some x => x end in (* previous_opt *) p; counter := previous; EmitCounterAsNumberend