module lambda where

open import Data.Nat

ll+_ : (x y : ℕ) → ℕ
ll+ zero = λ y → y
ll+ suc x = λ y → (ll+ x) (suc y)

test =  (ll+ 5) 7

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

+1 : (x : ℕ )→ ℕ
+1 x = suc x

+n : (a : ℕ) → (x : ℕ → ℕ) → ℕ
+n a x = x a

test*2 : (a : ℕ) → ℕ
test*2 a = +n a (λ z → z + 2)

test*2' : (a : ℕ) → ℕ
test*2' a = +n a (λ z → +n z (λ z → z))


λ'+2 : (x : ℕ) → ℕ
λ'+2 d = {!!} -- (λ x → x +1)