module spec GHC.Num where

GHC.Num.fromInteger :: (GHC.Num.Num a)
                    => x:GHC.Integer.Type.Integer
                    -> {v:a | v = x }

-- GHC.Num.negate :: (GHC.Num.Num a)
--                => x:a
--                -> {v:a | v = (0-x)}