Skip to content

Instantly share code, notes, and snippets.

@gallais
Forked from useronym/STLC.agda
Last active September 8, 2016 11:01
Show Gist options
  • Save gallais/d91f2ba131e0a788c3dcd50941a229b2 to your computer and use it in GitHub Desktop.
Save gallais/d91f2ba131e0a788c3dcd50941a229b2 to your computer and use it in GitHub Desktop.
module STLC (Atom : Set) (_≠_ : Atom → Atom → Set) where
open import Data.Empty
open import Data.Product as P hiding (_,_)
open import Data.List
open import Function hiding (_∋_)
data ★ : Set where
ι : ★
_⊳_ : ★ → ★ → ★
infixr 15 _⊳_
data Term : Set where
var : Atom → Term
ƛ_↦_ : Atom → Term → Term
_⋅_ : Term → Term → Term
infix 7 ƛ_↦_
infix 6 _⋅_
_﹕_ : ∀ {A B : Set} → A → B → A × B
_﹕_ = P._,_
infix 5 _﹕_
Cx : Set
Cx = List (Term × ★)
_,_ : {A : Set} → List A → A → List A
_,_ = flip _∷_
data _∋_ : Cx → (Atom × ★) → Set where
head : ∀ {Γ α x} → Γ , (var x ﹕ α) ∋ (x ﹕ α)
tail : ∀ {Γ α β x y} → x ≠ y → Γ ∋ (x ﹕ α) → Γ , (var y ﹕ β) ∋ (x ﹕ α)
data _⊢_ : Cx → (Term × ★) → Set where
VAR : ∀ {Γ α x} → Γ ∋ (x ﹕ α) → Γ ⊢ (var x ﹕ α)
LAM : ∀ {Γ α β x M} → Γ , (var x ﹕ α) ⊢ (M ﹕ β) → Γ ⊢ (ƛ x ↦ M ﹕ α ⊳ β)
APP : ∀ {Γ α β f x y} → Γ ⊢ (f ﹕ α ⊳ β) → Γ ⊢ (x ﹕ α) → Γ ⊢ (y ﹕ β)
infix 1 _⊢_ _∋_
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment