diff options
Diffstat (limited to 'src/Data/These')
| -rw-r--r-- | src/Data/These/Decidable.idr | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Data/These/Decidable.idr b/src/Data/These/Decidable.idr new file mode 100644 index 0000000..c044ca4 --- /dev/null +++ b/src/Data/These/Decidable.idr @@ -0,0 +1,16 @@ +module Data.These.Decidable + +import Data.Bool.Decidable +import Data.These + +export +viaEquivalence : a <=> b -> a `Reflects` x -> b `Reflects` x +viaEquivalence eq (RTrue x) = RTrue (eq.leftToRight x) +viaEquivalence eq (RFalse f) = RFalse (f . eq.rightToLeft) + +export +reflectThese : a `Reflects` x -> b `Reflects` y -> These a b `Reflects` x || y +reflectThese (RTrue x) (RTrue y) = RTrue (Both x y) +reflectThese (RTrue x) (RFalse ny) = RTrue (This x) +reflectThese (RFalse nx) (RTrue y) = RTrue (That y) +reflectThese (RFalse nx) (RFalse ny) = RFalse (these nx ny $ const ny) |