From 3a23bd851fc1a5d6e161dabc8a13f06bc8544a1d Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 9 Sep 2024 11:33:45 +0100 Subject: Restart. - use De Bruijn, as Namely, Painless had more pain than promised; - remove higher-kinded types; - provide ill-typing predicates; - prove substitution respects ill-typing; --- src/Data/These/Decidable.idr | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 src/Data/These/Decidable.idr (limited to 'src/Data/These/Decidable.idr') 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) -- cgit v1.2.3