Rerefined.Predicate.Relational

Documentation

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

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

Instances

(Typeable op, Typeable sign, KnownNat n) => Predicate (CompareValue op sign n :: Type)

Defined in Rerefined.Predicate.Relational.Value

Methods

predicateName :: Proxy# (CompareValue op sign n) -> Int -> ShowS

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

Defined in Rerefined.Predicate.Relational.Value

Methods

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

data Sign

Constructors

Pos

Neg

data RelOp

Relational operator.

There are three possible outcomes from compareing two terms, defined in Ordering. However, we may instead compare terms using relational operators such as >=, which are more specific comparisons that return a Bool.

Constructor order is arbitrary due to NEQ, which obstructs ordering in a meaningful way.

Constructors

LT'

< less than

LTE

<= less than or equal to

EQ'

== equal to

NEQ

/= less than or greater than

GTE

>= equal to or greater than

GT'

> greater than

data CompareLength (op :: RelOp) (n :: Natural)

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

Instances

(KnownNat n, Foldable f, ReifyRelOp op) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type)

Compare the length of a Foldable to a type-level Natural using the given RelOp.

Defined in Rerefined.Predicate.Relational.Length

Methods

validate1 :: forall (a :: k1). Proxy# (CompareLength op n) -> f a -> Maybe (RefineFailure String)

(Typeable op, KnownNat n) => Predicate (CompareLength op n :: Type)

Defined in Rerefined.Predicate.Relational.Length

Methods

predicateName :: Proxy# (CompareLength op n) -> Int -> ShowS

(KnownNat n, MonoFoldable a, ReifyRelOp op) => Refine (CompareLength op n :: Type) a

Compare the length of a MonoFoldable to a type-level Natural using the given RelOp.

Defined in Rerefined.Predicate.Relational.Length

Methods

validate :: Proxy# (CompareLength op n) -> a -> Maybe (RefineFailure String)