|
1
|
1 module lambda where
|
|
|
2
|
|
|
3 open import Data.Nat
|
|
|
4
|
|
|
5 ll+_ : (x y : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
|
|
|
6 ll+ zero = !$\lambda$! y !$\rightarrow$! y
|
|
|
7 ll+ suc x = !$\lambda$! y !$\rightarrow$! (ll+ x) (suc y)
|
|
|
8
|
|
|
9 test = (ll+ 5) 7
|
|
|
10
|
|
|
11 -- +1をしたのち，もう一度+1をする関数を定義する場合
|
|
|
12
|
|
|
13 +1 : (x : !$\mathbb{N}$! )!$\rightarrow$! !$\mathbb{N}$!
|
|
|
14 +1 x = suc x
|
|
|
15
|
|
|
16 +n : (a : !$\mathbb{N}$!) !$\rightarrow$! (x : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
|
|
|
17 +n a x = x a
|
|
|
18
|
|
|
19 test*2 : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
|
|
|
20 test*2 a = +n a (!$\lambda$! z !$\rightarrow$! z + 2)
|
|
|
21
|
|
3
|
22 test*2!$\prime$! : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
|
|
|
23 test*2!$\prime$! a = +n a (!$\lambda$! z !$\rightarrow$! +n z (!$\lambda$! z !$\rightarrow$! z))
|
|
1
|
24
|
|
|
25
|
|
3
|
26 !$\lambda$!!$\prime$!+2 : (x : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
|
|
|
27 !$\lambda$!!$\prime$!+2 d = {!!} -- (!$\lambda$! x !$\rightarrow$! x +1)
|
|
1
|
28
|
