
  0 | module TyRE.Extra.Pred
  1 | 
  2 | public export
  3 | Pred : Type -> Type
  4 | Pred a = (x : a) -> Type
  5 | 
  6 | infix 3 <->
  7 | ||| If and only if relation between predicates
  8 | public export
  9 | record (<->) {a : Type} (p, q : a -> Type) where
 10 |   constructor And
 11 |   If     : (x : a) -> (q x -> p x)
 12 |   onlyIf : (x : a) -> (p x -> q x)
 13 | 
 14 | infixr 4 /\
 15 | public export
 16 | (/\): {a: Type} -> (p : Pred a) -> (q : Pred a) -> Pred a
 17 | (/\) {a} p q x = (p x, q x)
 18 | 
 19 | infixr 4 \/
 20 | public export
 21 | (\/): {a: Type} -> (p : Pred a) -> (q : Pred a) -> Pred a
 22 | (\/) p q x = Either (p x) (q x)
 23 | 
 24 | public export
 25 | true: {a: Type} -> Pred a
 26 | true _ = Unit
 27 | 
 28 | public export
 29 | false: {a: Type} -> Pred a
 30 | false _ = Void
 31 |