
  0 | module Data.Bool.Rewrite
  1 | 
  2 | import public Data.Bool
  3 | 
  4 | %default total
  5 | 
  6 | public export %inline
  7 | swapOr : {0 x,y : _} -> (0 p : Bool -> Type) -> p (x || y) -> p (y || x)
  8 | swapOr p v = replace {p} (orCommutative x y) v
  9 | 
 10 | public export %inline
 11 | orSame : {0 x : _} -> (0 p : Bool -> Type) -> p (x || x) -> p x
 12 | orSame p v = replace {p} (orSameNeutral x) v
 13 | 
 14 | public export %inline
 15 | orTrue : {0 x : _} -> (0 p : Bool -> Type) -> p (x || True) -> p True
 16 | orTrue p v = replace {p} (orTrueTrue x) v
 17 | 
 18 | public export %inline
 19 | orFalse : {0 x : _} -> (0 p : Bool -> Type) -> p (x || False) -> p x
 20 | orFalse p v = replace {p} (orFalseNeutral x) v
 21 | 
 22 | public export %inline
 23 | swapAnd : {0 x,y : _} -> (0 p : Bool -> Type) -> p (x && y) -> p (y && x)
 24 | swapAnd p v = replace {p} (andCommutative x y) v
 25 | 
 26 | public export %inline
 27 | andSame : {0 x : _} -> (0 p : Bool -> Type) -> p (x && x) -> p x
 28 | andSame p v = replace {p} (andSameNeutral x) v
 29 | 
 30 | public export %inline
 31 | andTrue : {0 x : _} -> (0 p : Bool -> Type) -> p (x && True) -> p x
 32 | andTrue p v = replace {p} (andTrueNeutral x) v
 33 | 
 34 | public export %inline
 35 | andFalse : {0 x : _} -> (0 p : Bool -> Type) -> p (x && False) -> p False
 36 | andFalse p v = replace {p} (andFalseFalse x) v
 37 |