SmartLambda.agda

open import Data.Fin
open import Data.Nat
open import Function using (_∘_)

module SmartLambda where

data Term : ℕ → Set where
  var : ∀ {n} → Fin n → Term n
  lam : ∀ {n} → Term (suc n) → Term n
  _$_ : ∀ {n} → Term n → Term n → Term n
  wk : ∀ {n} → Term n → Term (suc n)

subst : ∀ {m n} → Term n → (Fin n → Term m) → Term m
subst (var i) s = s i
subst (lam b) s = lam (subst b λ { zero → var zero; (suc i) → wk (s i) })
subst (f $ x) s = subst f s $ subst x s
subst (wk x) s = subst x (s ∘ suc)

lam' : ∀ {n} → (∀ {m} → Fin (suc m) → Term (suc m)) → Term n
lam' b = lam (b zero)