Skip to content

Instantly share code, notes, and snippets.

@bvssvni

bvssvni/gist:11033561

Created April 18, 2014 09:17
Show Gist options
  • Save bvssvni/11033561 to your computer and use it in GitHub Desktop.
Save bvssvni/11033561 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.hs
data BitVector : Type where
MkBitVector : (bits : Integer) -> (value : Integer) ->
so (pow 2 (fromIntegerNat bits) > value) -> BitVector
test : BitVector
test = MkBitVector 2 3 oh
-- How do I get information out?
-- Does it need more type information, like something after '-> BitVector'?
@edwinb
Copy link

edwinb commented Apr 18, 2014 

getBits : BitVector -> Integer
getBits (MkBitVector b v prf) = b

getVal : BitVector -> Integer
getVal (MkBitVector b v prf) = v

getPrf : (bv : BitVector) ->
         so (pow 2 (fromIntegerNat (getBits bv)) > (getVal bv))
getPrf (MkBitVector b v prf) = prf

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment