blob: 229acf8427cba81b477f45fb42a9d3d062dd10e4 (
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
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the case expressions can be used
------------------------------------------------------------------------
module README.Case where
open import Data.Fin hiding (pred)
open import Data.Maybe hiding (from-just)
open import Data.Nat hiding (pred)
open import Function
-- Some simple examples.
empty : ∀ {a} {A : Set a} → Fin 0 → A
empty i = case i of λ()
pred : ℕ → ℕ
pred n = case n of λ
{ zero → zero
; (suc n) → n
}
from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just x
from-just x = case x return From-just of λ
{ (just x) → x
; nothing → _
}
-- Note that some natural uses of case are rejected by the termination
-- checker:
--
-- plus : ℕ → ℕ → ℕ
-- plus m n = case m of λ
-- { zero → n
-- ; (suc m) → suc (plus m n)
-- }
|
