Rerefined.Predicate.Relational.Internal

Documentation

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

class Typeable op => ReifyRelOp (op :: RelOp) where

Reify a relational operator type tag.

We stuff the Typeable constraint in here because we need it for easy Predicate instances, and we don't want to expose the Typeable constraint elsewhere.

Methods

reifyRelOp :: forall a. (Num a, Ord a) => a -> a -> Bool

The term-level relational operator that op describes.

reifyRelOpPretty :: String

Pretty operator.

Instances

ReifyRelOp 'EQ'

Defined in Rerefined.Predicate.Relational.Internal

Methods

reifyRelOp :: (Num a, Ord a) => a -> a -> Bool

reifyRelOpPretty :: String

ReifyRelOp 'GT'

Defined in Rerefined.Predicate.Relational.Internal

Methods

reifyRelOp :: (Num a, Ord a) => a -> a -> Bool

reifyRelOpPretty :: String

ReifyRelOp 'GTE

Defined in Rerefined.Predicate.Relational.Internal

Methods

reifyRelOp :: (Num a, Ord a) => a -> a -> Bool

reifyRelOpPretty :: String

ReifyRelOp 'LT'

Defined in Rerefined.Predicate.Relational.Internal

Methods

reifyRelOp :: (Num a, Ord a) => a -> a -> Bool

reifyRelOpPretty :: String

ReifyRelOp 'LTE

Defined in Rerefined.Predicate.Relational.Internal

Methods

reifyRelOp :: (Num a, Ord a) => a -> a -> Bool

reifyRelOpPretty :: String

ReifyRelOp 'NEQ

Defined in Rerefined.Predicate.Relational.Internal

Methods

reifyRelOp :: (Num a, Ord a) => a -> a -> Bool

reifyRelOpPretty :: String

type family WidenRelOp (op :: RelOp) (n :: Natural) (m :: Natural) where ...

Can we widen the given RelOp from n to m?

Equations

WidenRelOp op n n = True

WidenRelOp LT' n m = OrdCond (CmpNat n m) True True False

WidenRelOp LTE n m = OrdCond (CmpNat n m) True True False

WidenRelOp GTE n m = OrdCond (CmpNat n m) False True True

WidenRelOp GT' n m = OrdCond (CmpNat n m) False True True

WidenRelOp _ _ _ = False