/
Maybe.agda
41 lines (30 loc) · 1.11 KB
/
Maybe.agda
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
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Maybe where
open import Data.Empty using (⊥)
open import Data.Unit.Base using (⊤)
open import Data.Bool.Base using (T)
open import Data.Maybe.Relation.Unary.All using (All)
open import Data.Maybe.Relation.Unary.Any using (Any; just)
open import Level using (Level)
private
variable
a : Level
A : Set a
------------------------------------------------------------------------
-- The base type and some operations
open import Data.Maybe.Base public
------------------------------------------------------------------------
-- Using Any and All to define Is-just and Is-nothing
Is-just : Maybe A → Set _
Is-just = Any (λ _ → ⊤)
Is-nothing : Maybe A → Set _
Is-nothing = All (λ _ → ⊥)
to-witness : ∀ {m : Maybe A} → Is-just m → A
to-witness (just {x = p} _) = p
to-witness-T : ∀ (m : Maybe A) → T (is-just m) → A
to-witness-T (just p) _ = p