module Counter where

open import Nat

-- the following is a record type implementing the abstract data type for-- counters in Pierce chapter 24. It serves the same role as the 
-- existential type in Pierce

record counterADT : Set1 where
  field
    Counter : Set
    new : Counter
    get : Counter -> Nat
    inc : Counter -> Counter

-- an implementation of an abstract data type is an element of the 
-- record implementing it. Again, note the similarity with elements of
-- existential types in Pierce

natCounter : counterADT
natCounter = record { Counter = Nat
                    ; new = zero
                    ; get = λ n → n
                    ; inc = succ
                    }