module UntypedLambdaExpr where

open import Nat
open import Fin
------------------------------------------------------------------------
-- The untyped λ-calculus
------------------------------------------------------------------------

-- Syntax

-- Variables are represented using de Bruijn indices. Term n stands
-- for terms with at most n distinct free variables.
-- Here is an implementation of Def 6.1.2 in Pierce

data Term (n : Nat) : Set where
  var : Fin n → Term n
  lam : Term (succ n) → Term n
  app : Term n → Term n → Term n

-- Examples.

id : Term zero
id = lam (var zero)  -- λx.x

k : Term zero
k = lam (lam (var (suc zero))) -- λxy.x

ω : Term zero
ω = lam (app (var zero) (var zero))  -- λx.xx

Ω : Term zero
Ω = app ω ω  -- (λx.xx) (λx.xx)