rerefined-0.4.0: Refinement types, again
Safe HaskellSafe-Inferred
LanguageGHC2021

Rerefined.Predicate.Relational

Synopsis

Documentation

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

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

Instances

Instances details
Predicate (CompareValue op sign n :: Type) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Value

Associated Types

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

(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, KnownPredicateName (CompareValue op sign n)) => 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 Source #

type PredicateName d (CompareValue op sign n :: Type) Source # 
Instance details

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 Source #

Constructors

Pos 
Neg 

data CompareLength op (n :: Natural) Source #

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

Instances

Instances details
(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Length

Methods

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

Predicate (CompareLength op n :: Type) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Length

Associated Types

type PredicateName d (CompareLength op n) :: Symbol Source #

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

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

Instance details

Defined in Rerefined.Predicate.Relational.Length

type PredicateName d (CompareLength op n :: Type) Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Length

type PredicateName d (CompareLength op n :: Type) = ShowParen (d > 4) ((("Length " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowNatDec n)

type LTE = LT `Or` EQ Source #

type GTE = GT `Or` EQ Source #