blob: c044ca46c03f4b05bb96947db2b5d47e9d2db433 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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)
|
