module DeBruijn where

data Term = Var Int
          | App Term Term
          | Abs Term
  deriving Eq


subst i t (Var j) = if i == j then t else Var j
subst i t (App t1 t2) = App (subst i t t1) (subst i t t1)
subst i t (Abs t2) = Abs (subst (i + 1) t t2)

beta :: Term -> Term
beta (Var i) = Var i
beta (Abs t) = Abs t 
beta (App (Var v) t2) = (App (Var v) t2)
beta (App (App t1 t2) t3) = App (beta (App t1 t2)) t3 
beta (App (Abs t) t2) = subst 0 t t2