liquid-base-4.14.3.0: src/GHC/Num.spec

module spec GHC.Num where

embed GHC.Integer.Type.Integer as int
embed GHC.Num.Integer as int

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

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

GHC.Num.+ :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x + y }
GHC.Num.- :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x - y }