55 lines
830 B
Text
55 lines
830 B
Text
---
|
||
title : "Inherent"
|
||
layout : page
|
||
permalink : /Inherent/
|
||
---
|
||
|
||
\begin{code}
|
||
module plfa.Inherent where
|
||
|
||
infix 4 _⊢_
|
||
infix 4 _∋_
|
||
infixl 5 _,_
|
||
\end{code}
|
||
|
||
## WTF
|
||
|
||
\begin{code}
|
||
data Type : Set where
|
||
_⇒_ : Type → Type → Type
|
||
`ℕ : Type
|
||
|
||
data Context : Set where
|
||
∅ : Context
|
||
_,_ : Context → Type → Context
|
||
|
||
data _∋_ : Context → Type → Set where
|
||
|
||
Z : ∀ {Γ A}
|
||
----------
|
||
→ Γ , A ∋ A
|
||
|
||
S_ : ∀ {Γ A B}
|
||
→ Γ ∋ A
|
||
---------
|
||
→ Γ , B ∋ A
|
||
|
||
data _⊢_ : Context → Type → Set where
|
||
|
||
`_ : ∀ {Γ} {A}
|
||
→ Γ ∋ A
|
||
------
|
||
→ Γ ⊢ A
|
||
|
||
ƛ_ : ∀ {Γ} {A B}
|
||
→ Γ , A ⊢ B
|
||
----------
|
||
→ Γ ⊢ A ⇒ B
|
||
|
||
_·_ : ∀ {Γ} {A B}
|
||
→ Γ ⊢ A ⇒ B
|
||
→ Γ ⊢ A
|
||
----------
|
||
→ Γ ⊢ B
|
||
\end{code}
|
||
|