Skip to content

Instantly share code, notes, and snippets.

@useronym
Created September 8, 2016 08:37
  • Star 0 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save useronym/7db4067edb4e199e5657431dffca6de1 to your computer and use it in GitHub Desktop.
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
_﹕_ = ⟨_,_⟩
infix 5 _﹕_
Cx : Set
Cx = List (Term × ★)
data _⊢_ : Cx → (Term × ★) → Set where
VAR : ∀ {Γ α x} → Γ , (var x ﹕ α) ⊢ (var x ﹕ α)
LAM : ∀ {Γ α β x M} → Γ , (var x ﹕ α) ⊢ (M ﹕ β) → Γ ⊢ (ƛ x ↦ M ﹕ α ⊳ β)
APP : ∀ {Γ α β f x y} → Γ ⊢ (f ﹕ α ⊳ β) → Γ ⊢ (x ﹕ α) → Γ ⊢ (y ﹕ β)
infix 1 _⊢_
-- Free variables in a term.
FV : ∀ {Γ A} → Γ ⊢ A → List Atom
FV (VAR {x = a}) = [ a ]
FV (LAM {x = a} t) = (FV t) - a
FV (APP t₁ t₂) = (FV t₁) ∪ (FV t₂)
-- λI terms.
λI : ∀ {Γ A} → Γ ⊢ A → Set
λI VAR = ⊤
λI (LAM {x = a} t) = (λI t) × (a ∈ (FV t))
λI (APP t₁ t₂) = (λI t₁) × (λI t₂)
Closed : (Term × ★) → Set
Closed = _⊢_ ∅
I : Closed ((ƛ v₀ ↦ (var v₀)) ﹕ (ι ⊳ ι))
I = LAM VAR
I-is-λI : λI I
I-is-λI = ⟨ • , zero ⟩
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment