From fb37a9b65813666a3963c240a1bc8f6978a4866f Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 24 Apr 2021 13:55:33 +0100 Subject: Modify Fin definitions. --- src/Cfe/Context/Base.agda | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) (limited to 'src/Cfe/Context/Base.agda') diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda index e152790..9f3a197 100644 --- a/src/Cfe/Context/Base.agda +++ b/src/Cfe/Context/Base.agda @@ -13,7 +13,7 @@ open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁) open import Data.Nat using (ℕ; suc; _∸_; _+_) open import Data.Nat.Properties using (+-suc) open import Data.Product using (_×_) -open import Data.Vec using (Vec; []; insert) +open import Data.Vec using (Vec; []; insert; remove) open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise) open import Level renaming (suc to lsuc) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; module ≡-Reasoning) @@ -43,16 +43,25 @@ open Context public -- Insertions wkn₂ : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Type ℓ ℓ → Context (suc n) -wkn₂ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (inject (guard ctx) → Type ℓ ℓ → Context (suc n) -wkn₁ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (raise> i) τ ⊐ inject₁ g +wkn₁ : ∀ (ctx : Context n) → Fin> (inject₁ (guard ctx)) → Type ℓ ℓ → Context (suc n) +wkn₁ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (raise!> i) τ ⊐ inject₁ g ------------------------------------------------------------------------ -- Modifications shift : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Context n -shift (Γ,Δ ⊐ _) i = Γ,Δ ⊐ inject (guard ctx) → Context n +remove₁ (Γ,Δ ⊐ g) i = remove Γ,Δ (raise!> i) ⊐ inject₁ⁱ> i ------------------------------------------------------------------------ -- Relations -- cgit v1.2.3