module Lambda(Node : Set) where
open import GeneralLemmas

infixl 1 _$_

data Term : Set where
  ƛ_    : Term  Term
  _$_   : (t t' : Term)  Term
  var   :   Term
  lit   :   Term                              -- natural numbers
  op    : (f :     )(t t' : Term)  Term
  if0_then_else_  : (b t f : Term)  Term
  _at_  : Term  Node  Term

data Value : Set where     -- canonical lambda terms
  ƛ_  : Term  Value
  lit :   Value

value : Value  Term
value (ƛ t) = ƛ t
value (lit n) = lit n