module lambda where

open import Data.Nat

ll+_ : (x y : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
ll+ zero = !$\lambda$! y !$\rightarrow$! y
ll+ suc x = !$\lambda$! y !$\rightarrow$! (ll+ x) (suc y)

test =  (ll+ 5) 7

-- +1をしたのち，もう一度+1をする関数を定義する場合

+1 : (x : !$\mathbb{N}$! )!$\rightarrow$! !$\mathbb{N}$!
+1 x = suc x

+n : (a : !$\mathbb{N}$!) !$\rightarrow$! (x : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
+n a x = x a

test*2 : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
test*2 a = +n a (!$\lambda$! z !$\rightarrow$! z + 2)

test*2!$\prime$! : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
test*2!$\prime$! a = +n a (!$\lambda$! z !$\rightarrow$! +n z (!$\lambda$! z !$\rightarrow$! z))


!$\lambda$!!$\prime$!+2 : (x : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
!$\lambda$!!$\prime$!+2 d = {!!} -- (!$\lambda$! x !$\rightarrow$! x +1)