Data.Refined.Core

Reexports

Definitions

data Always : a -> Type

  The predicate that always holds.

Totality: total
Visibility: public export
Constructor: 

Yes : Always a

Hints:

HDec a Always

HDec0 a Always

data Never : a -> Type

  The predicate that never holds.

Totality: total
Visibility: public export
Hints:

HDec a Never

HDec0 a Never

data (&&) : (a -> Type) -> (a -> Type) -> a -> Type

  Conjunction of two predicates

Totality: total
Visibility: public export
Constructor: 

And : (v `p`) -> q v -> (&&) p q v

Hints:

HDec a p => HDec a q => HDec a (p && q)

HDec0 a p => HDec0 a q => HDec0 a (p && q)

Fixity Declaration: infixr operator, level 5

mapFst : ((x `p`) -> r x) -> (&&) p q x -> (&&) r q x

Totality: total
Visibility: public export

mapSnd : (q x -> r x) -> (&&) p q x -> (&&) p r x

Totality: total
Visibility: public export

data (||) : (a -> Type) -> (a -> Type) -> a -> Type

  Disjunction of two predicates

Totality: total
Visibility: public export
Constructors:

L : (v `p`) -> (||) p q v

R : q v -> (||) p q v

Hints:

HDec a p => HDec a q => HDec a (p || q)

HDec0 a p => HDec0 a q => HDec0 a (p || q)

Fixity Declaration: infixr operator, level 4

mapL : ((x `p`) -> r x) -> (||) p q x -> (||) r q x

Totality: total
Visibility: public export

mapR : (q x -> r x) -> (||) p q x -> (||) p r x

Totality: total
Visibility: public export

deMorgan1 : Not ((||) p q v) -> (&&) (Not . p) (Not . q) v

Totality: total
Visibility: export

data On : (a -> Type) -> (b -> a) -> b -> Type

Totality: total
Visibility: public export
Constructor: 

HoldsOn : (f v `p`) -> On p f v

Hints:

HDec a p => HDec b (On p f)

HDec0 a p => HDec0 b (On p f)

mapOn : ((f x `p`) -> q (f x)) -> On p f x -> On q f x

Totality: total
Visibility: public export

data Holds : (a -> Bool) -> a -> Type

  Proof that an (explicitly given) boolean predicate holds

Totality: total
Visibility: public export
Constructor: 

ItHolds : f v = True -> Holds f v

Hints:

HDec a (Holds f)

HDec0 a (Holds f)

test : (b : Bool) -> Maybe0 (b = True)

Totality: total
Visibility: public export

0 holdsAnd : (v : a) -> (&&) (Holds f) (Holds g) v -> Holds (\x => f x && Delay (g x)) v

  Conversion from type-level `(&&)` to boolean `(&&)`

Totality: total
Visibility: export

0 andHolds : (v : a) -> Holds (\x => f x && Delay (g x)) v -> (&&) (Holds f) (Holds g) v

  Conversion from boolean `(&&)` to type-level `(&&)`

Totality: total
Visibility: export

0 holdsOr : (v : a) -> (||) (Holds f) (Holds g) v -> Holds (\x => f x || Delay (g x)) v

  Conversion from type-level `(||)` to boolean `(||)`

Totality: total
Visibility: export

0 orHolds : (v : a) -> Holds (\x => f x || Delay (g x)) v -> (||) (Holds f) (Holds g) v

  Conversion from boolean `(||)` to type-level `(||)`

Totality: total
Visibility: export

data Const : (e -> Type) -> e -> t -> Type

  The `Const` predicate.
  
  This allows us to refine a value based on a refinement on a second
  value.

Totality: total
Visibility: public export
Constructor: 

C : (v `p`) -> Const p v x

Hint: 

HDec0 e p => HDec0 t (Const p v)

unConst : Const p v t -> (v `p`)

Totality: total
Visibility: public export

refine0 : HDec0 a p => a -> Maybe (Subset a p)

  Try to refine a value into a `Subset`.

Totality: total
Visibility: public export

refine : HDec a p => a -> Maybe (DPair a p)

  Try to refine a value into a `DPair`.

Totality: total
Visibility: public export