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
|
<h2>Full example</h2>
<pre><code>
-- source: https://github.com/dhall-lang/dhall-lang/blob/master/Prelude/Optional/head.dhall
{-
Returns the first non-empty `Optional` value in a `List`
-}
let head
: ∀(a : Type) → List (Optional a) → Optional a
= λ(a : Type) →
λ(xs : List (Optional a)) →
List/fold
(Optional a)
xs
(Optional a)
( λ(l : Optional a) →
λ(r : Optional a) →
merge { Some = λ(x : a) → Some x, None = r } l
)
(None a)
let example0 = assert : head Natural [ None Natural, Some 1, Some 2 ] ≡ Some 1
let example1 =
assert : head Natural [ None Natural, None Natural ] ≡ None Natural
let example2 =
assert : head Natural ([] : List (Optional Natural)) ≡ None Natural
in head</code></pre>
|
