diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-12 18:05:25 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-12 18:05:25 +0000 |
| commit | 6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd (patch) | |
| tree | f1704be1e5adef266693429898408bfa4b320688 /src/Inky/Decidable/Either.idr | |
| parent | ecaf9deb4b1d2ce85617438e621690b2df3ea367 (diff) | |
Add more names. Names are good.
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 |