module spec GHC.Prim where

embed GHC.Prim.Int#  as int
embed GHC.Prim.Word# as int
embed GHC.Prim.Addr# as int

embed GHC.Prim.Double#  as real

measure addrLen :: GHC.Prim.Addr# -> GHC.Types.Int

assume GHC.Types.I# :: x:GHC.Prim.Int# -> {v: GHC.Types.Int | v = (x :: int) }
assume GHC.Prim.+#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x + y}
assume GHC.Prim.-#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x - y}
assume GHC.Prim.==# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int#
                    -> {v:GHC.Prim.Int# | ((v = 1) <=> x = y)}
assume GHC.Prim.>=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# 
                    -> {v:GHC.Prim.Int# | ((v = 1) <=> x >= y)}
assume GHC.Prim.<=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# 
                    -> {v:GHC.Prim.Int# | ((v = 1) <=> x <= y)}
assume GHC.Prim.<#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# 
                    -> {v:GHC.Prim.Int# | ((v = 1) <=> x < y)}
assume GHC.Prim.>#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# 
                    -> {v:GHC.Prim.Int# | ((v = 1) <=> x > y)}