Bound.agda

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′