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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the case expressions can be used with anonymous
-- pattern-matching lambda abstractions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
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.Base using (case_of_; case_returning_of_)
open import Relation.Nullary
------------------------------------------------------------------------
-- Different types of pattern-matching lambdas
-- absurd pattern
empty : ∀ {a} {A : Set a} → Fin 0 → A
empty i = case i of λ ()
-- {}-delimited and ;-separated list of clauses
-- Note that they do not need to be on different lines
pred : ℕ → ℕ
pred n = case n of λ
{ zero → zero
; (suc n) → n
}
-- where-introduced and indentation-identified block of list of clauses
from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just x
from-just x = case x returning From-just of λ where
(just x) → x
nothing → _
------------------------------------------------------------------------
-- We can define some recursive functions with case
plus : ℕ → ℕ → ℕ
plus m n = case m of λ
{ zero → n
; (suc m) → suc (plus m n)
}
div2 : ℕ → ℕ
div2 zero = zero
div2 (suc m) = case m of λ where
zero → zero
(suc m′) → suc (div2 m′)
-- Note that some natural uses of case are rejected by the termination
-- checker:
-- module _ {a} {A : Set a} (eq? : Decidable {A = A} _≡_) where
-- pairBy : List A → List (A ⊎ (A × A))
-- pairBy [] = []
-- pairBy (x ∷ []) = inj₁ x ∷ []
-- pairBy (x ∷ y ∷ xs) = case eq? x y of λ where
-- (yes _) → inj₂ (x , y) ∷ pairBy xs
-- (no _) → inj₁ x ∷ pairBy (y ∷ xs)
|
