blob: 0820d4233c7c8b62b535d116a3b7ea4e69f34796 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary using (Rel; REL; Setoid)
module Cfe.Judgement.Base
{c ℓ} (over : Setoid c ℓ)
where
open import Cfe.Context over
open import Cfe.Expression over
open import Cfe.Fin using (zero; raise!>)
open import Cfe.Type over renaming (_∙_ to _∙ᵗ_; _∨_ to _∨ᵗ_)
open import Data.Fin using (inject₁)
open import Data.Nat using (ℕ; suc)
open import Data.Product using (∃-syntax)
open import Data.Vec using (lookup)
open import Level using (_⊔_) renaming (suc to lsuc)
infix 2 _⊢_∶_
private
variable
n : ℕ
ctx : Context n
data _⊢_∶_ : {n : ℕ} → Context n → Expression n → Type ℓ ℓ → Set (c ⊔ lsuc ℓ) where
Eps : ctx ⊢ ε ∶ τε
Char : ∀ c → ctx ⊢ Char c ∶ τ[ c ]
Bot : ctx ⊢ ⊥ ∶ τ⊥
Var : ∀ j → ctx ⊢ Var (raise!> {i = guard ctx} j) ∶ lookup (Γ,Δ ctx) (raise!> j)
Fix : ∀ {e τ} → wkn₂ ctx zero τ ⊢ e ∶ τ → ctx ⊢ μ e ∶ τ
Cat : ∀ {e₁ e₂ τ₁ τ₂} →
ctx ⊢ e₁ ∶ τ₁ →
shift ctx zero ⊢ e₂ ∶ τ₂ →
(τ₁⊛τ₂ : τ₁ ⊛ τ₂) →
ctx ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ᵗ τ₂
Vee : ∀ {e₁ e₂ τ₁ τ₂} →
ctx ⊢ e₁ ∶ τ₁ →
ctx ⊢ e₂ ∶ τ₂ →
(τ₁#τ₂ : τ₁ # τ₂) →
ctx ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ᵗ τ₂
|
