Rerefined.Predicate.Relational.Value

Documentation

data CompareValue op (sign :: Sign) (n :: Natural)

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

Instances

Predicate (CompareValue op sign n :: Type)

Precedence of 4 (matching base relational operators e.g. >=).

Defined in Rerefined.Predicate.Relational.Value

Associated Types

type PredicateName d (CompareValue op sign n) :: Symbol

(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, KnownPredicateName (CompareValue op sign n)) => Refine (CompareValue op sign n :: Type) a

Defined in Rerefined.Predicate.Relational.Value

Methods

validate :: Proxy# (CompareValue op sign n) -> a -> Maybe RefineFailure

type PredicateName d (CompareValue op sign n :: Type)

Defined in Rerefined.Predicate.Relational.Value

type PredicateName d (CompareValue op sign n :: Type) = ShowParen (d > 4) (((("Value " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowSign sign) ++ ShowNatDec n)

data Sign

Constructors

Pos

Neg

type family ShowSign (sign :: Sign) :: Symbol where ...

Equations

ShowSign Pos = ""

ShowSign Neg = "-"

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

Methods

reifySignedNat :: (Num a, KnownNat n) => a

Instances

ReifySignedNat 'Neg n

Defined in Rerefined.Predicate.Relational.Value

Methods

reifySignedNat :: (Num a, KnownNat n) => a

ReifySignedNat 'Pos n

Defined in Rerefined.Predicate.Relational.Value

Methods

reifySignedNat :: (Num a, KnownNat n) => a