Safe Haskell	Safe-Inferred
Language	GHC2021

Rerefined.Predicate.Relational.Value

Synopsis

data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural)
data Sign
- = Pos
- | Neg
class Typeable sign => ReifySign (sign :: Sign) where
- signPretty :: String
class ReifySignedNat (sign :: Sign) (n :: Natural) where
- reifySignedNat :: (Num a, KnownNat n) => a

Documentation

Compare value to a type-level Natural using the given RelOp.

Instances details

(Typeable op, Typeable sign, KnownNat n) => Predicate (CompareValue op sign n :: Type) Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods predicateName :: Proxy# (CompareValue op sign n) -> Int -> ShowS Source #
(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, ReifySign sign) => Refine (CompareValue op sign n :: Type) a Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods validate :: Proxy# (CompareValue op sign n) -> a -> Maybe (RefineFailure String) Source #

Constructors

Pos
Neg

class Typeable sign => ReifySign (sign :: Sign) where Source #

Methods

Instances details

ReifySign 'Neg Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods signPretty :: String Source #
ReifySign 'Pos Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods signPretty :: String Source #

class ReifySignedNat (sign :: Sign) (n :: Natural) where Source #

Methods

Instances details

ReifySignedNat 'Neg n Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods reifySignedNat :: (Num a, KnownNat n) => a Source #
ReifySignedNat 'Pos n Source #
Instance details Defined in Rerefined.Predicate.Relational.Value Methods reifySignedNat :: (Num a, KnownNat n) => a Source #