diff options
Diffstat (limited to 'src/Inky/Decidable/Either.idr')
| -rw-r--r-- | src/Inky/Decidable/Either.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Inky/Decidable/Either.idr b/src/Inky/Decidable/Either.idr index 9da2c72..bea3364 100644 --- a/src/Inky/Decidable/Either.idr +++ b/src/Inky/Decidable/Either.idr @@ -1,5 +1,6 @@ module Inky.Decidable.Either +import Data.So import Data.These public export @@ -88,6 +89,10 @@ public export any : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (These a c) (b, d) any p q = p.does || q.does `Because` Union.any p.reason q.reason +public export +so : (b : Bool) -> LazyEither (So b) (So $ not b) +so b = b `Because` if b then Oh else Oh + export autobind infixr 0 >=> public export |