Syntax.agda

module STLC.Syntax (Type : Set) where

open import Data.String

Name : Set
Name = String

data Formal : Set where
  _∶_ : Name → Type → Formal

data Expr : Set where
  var : Name → Expr
  lam : Formal → Expr → Expr
  _·_ : Expr → Expr → Expr
infixl 20 _·_