From 6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 12 Nov 2024 18:05:25 +0000 Subject: Add more names. Names are good. --- src/Inky/Decidable/Either.idr | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Inky/Decidable/Either.idr') 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 -- cgit v1.2.3