NomPa.Examples.Raw

open import Data.String
open import Data.List
open import Data.Nat

module NomPa.Examples.Raw where

infixl 4 _·_
data Tmᴿ : Set where
  V : (x : String) → Tmᴿ
  ƛ : (b : String) (t : Tmᴿ) → Tmᴿ
  _·_ : (t u : Tmᴿ) → Tmᴿ

appⁿ : Tmᴿ → List Tmᴿ → Tmᴿ
appⁿ = foldl _·_

_ℕᴿ : ℕ → Tmᴿ
n ℕᴿ = ƛ "f" (ƛ "x" (replicapp n (V "f") (V "x")))
  where replicapp : ℕ → Tmᴿ → Tmᴿ → Tmᴿ
        replicapp zero    t u = u
        replicapp (suc n) t u = t · replicapp n t u