gistfile1.hs

-- describes an Integer representation of Bools
-- that also specify how many bits are used
data BitVector : Integer -> Integer -> Type

-- I want to make sure that the value of the integer
-- is always less than 2^first_argument.
-- Is this possible?

-- takes two Bool and return an Integer.
pairOfBoolsToInteger : Bool -> Bool -> BitVector 2 Integer
pairOfBoolsToInteger a b = case (a, b) of
  (False, False) => 0
  (True, False) => 1
  (False, True) => 2
  (True, True) => 3