TyRE.Extra.Pred

Definitions

Pred : Type -> Type

Visibility: public export

record (<->) : (a -> Type) -> (a -> Type) -> Type

  If and only if relation between predicates

Totality: total
Visibility: public export
Constructor: 

And : ((x : a) -> q x -> p x) -> ((x : a) -> p x -> q x) -> p <-> q

Projections:

.If : p <-> q -> (x : a) -> q x -> p x

.onlyIf : p <-> q -> (x : a) -> p x -> q x

Fixity Declaration: infix operator, level 3

.If : p <-> q -> (x : a) -> q x -> p x

Visibility: public export

If : p <-> q -> (x : a) -> q x -> p x

Visibility: public export

.onlyIf : p <-> q -> (x : a) -> p x -> q x

Visibility: public export

onlyIf : p <-> q -> (x : a) -> p x -> q x

Visibility: public export

(/\) : Pred a -> Pred a -> Pred a

Visibility: public export
Fixity Declaration: infixr operator, level 4

(\/) : Pred a -> Pred a -> Pred a

Visibility: public export
Fixity Declaration: infixr operator, level 4

true : Pred a

Visibility: public export

false : Pred a

Visibility: public export