diff options
Diffstat (limited to 'src/Cfe/Judgement/Base.agda')
| -rw-r--r-- | src/Cfe/Judgement/Base.agda | 42 |
1 files changed, 28 insertions, 14 deletions
diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda index 4be0256..0820d42 100644 --- a/src/Cfe/Judgement/Base.agda +++ b/src/Cfe/Judgement/Base.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary using (Setoid) +open import Relation.Binary using (Rel; REL; Setoid) module Cfe.Judgement.Base {c ℓ} (over : Setoid c ℓ) @@ -8,20 +8,34 @@ module Cfe.Judgement.Base open import Cfe.Context over open import Cfe.Expression over -open import Cfe.Type over renaming (_∙_ to _∙ₜ_; _∨_ to _∨ₜ_) -open import Cfe.Type.Construct.Lift over -open import Data.Fin as F -open import Data.Nat hiding (_⊔_) -open import Data.Vec hiding (_⊛_) -open import Level hiding (Lift) renaming (suc to lsuc) +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 : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ε ∶ Lift ℓ ℓ τε - Char : ∀ {n} {Γ,Δ : Context n} c → Γ,Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ] - Bot : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥ - Var : ∀ {n} {Γ,Δ : Context n} {i} (i≥m : toℕ i ≥ _) → Γ,Δ ⊢ Var i ∶ lookup (Context.Γ Γ,Δ) (reduce≥′ (Context.m≤n Γ,Δ) i≥m) - Fix : ∀ {n} {Γ,Δ : Context n} {e τ} → cons Γ,Δ τ ⊢ e ∶ τ → Γ,Δ ⊢ μ e ∶ τ - Cat : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → shift Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁⊛τ₂ : τ₁ ⊛ τ₂) → Γ,Δ ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ₜ τ₂ - Vee : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ,Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂ + 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₂ ∶ τ₁ ∨ᵗ τ₂ |