Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Synopsis
- module Rerefined.Refine
- module Rerefined.Refine.TH
- class Predicate p
- class Predicate p => Refine p a
- class Predicate p => Refine1 p f
Documentation
module Rerefined.Refine
module Rerefined.Refine.TH
Types which define refinements on other types.
Instances
class Predicate p => Refine p a Source #
Refine a
with predicate p
.
Instances
class Predicate p => Refine1 p f Source #
Refine functor type f
with functor predicate p
.
By not making the contained type accessible, we ensure refinements apply
forall a. f a
. That is, refinements here apply only to the functor
structure, and not the stored elements.
Instances
(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source # | Compare the length of a |
Defined in Rerefined.Predicate.Relational.Length validate1 :: forall (a :: k1). Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure Source # |