module STLC.Bound (Type : Set) where

open import STLC.Syntax Type as S hiding (Expr; module Expr)

open import Data.Nat hiding (_≟_)
open import Data.Fin
open import Data.Vec
open import Data.String
open import Relation.Nullary.Decidable

data Expr (n : ) : Set where
  var : (k : Fin n)  Expr n
  lam : (τ : Type)  Expr (suc n)  Expr n
  _·_ : Expr n  Expr n  Expr n
infixl 20 _·_

Binder :   Set
Binder = Vec Name

data _⊢_↝_ :  {n}  Binder n  S.Expr  Expr n  Set where
  var-zero :  {n x} {Γ : Binder n} 
             (x  Γ)  var x  var zero

  var-suc  :  {n x y k} {Γ : Binder n} {p : False (x  y)} 
             Γ  var x  var k 
             (y  Γ)  var x  var (suc k)

  lam      :  {n x τ E E′} {Γ : Binder n} 
             (x  Γ)  E  E′ 
             Γ  (lam (x  τ) E)  (lam τ E′)

  _·_      :  {n E E′ F F′} {Γ : Binder n} 
             Γ  E  E′ 
             Γ  F  F′ 
             Γ  E · F  E′ · F′