blob: 7bed91a787f6fab0af4bc2b62404ea9f411aa2f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
module Inky.OnlyWhen
import Data.DPair
public export
data OnlyWhen : Maybe a -> (a -> Type) -> Type where
Yes : forall x. (px : p x) -> Just x `OnlyWhen` p
No : ((x : a) -> Not (p x)) -> Nothing `OnlyWhen` p
public export
decDPair : (v ** v `OnlyWhen` p) <=> Dec (x : a ** p x)
decDPair =
MkEquivalence
{ leftToRight = \case
(Just x ** Yes px) => Yes (x ** px)
(Nothing ** No prf) => No (\(x ** px) => prf x px)
, rightToLeft = \case
Yes (x ** px) => (Just x ** Yes px)
No prf => (Nothing ** No (\x, px => prf (x ** px)))
}
public export
decExists : Exists (`OnlyWhen` p) <=> Dec (Exists p)
decExists =
MkEquivalence
{ leftToRight = \case
Evidence .(Just x) (Yes px) => Yes (Evidence x px)
Evidence .(Nothing) (No prf) => No (\(Evidence x px) => void (prf x px))
, rightToLeft = \case
Yes (Evidence x px) => Evidence (Just x) (Yes px)
No prf => Evidence Nothing (No (\x, px => prf (Evidence x px)))
}
public export
decSubset : Subset (Maybe a) (`OnlyWhen` p) <=> Dec (Subset a p)
decSubset =
MkEquivalence
{ leftToRight = \case
Element (Just x) prf => Yes (Element x (case prf of Yes px => px))
Element Nothing prf => No (\(Element x px) => void (case prf of No prf => prf x px))
, rightToLeft = \case
Yes (Element x px) => Element (Just x) (Yes px)
No prf => Element Nothing (No (\x, px => prf (Element x px)))
}
|
