From c70e990c29ec1957b26ab647825e6026f568e8bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 24 Oct 2020 17:02:29 +0200 Subject: [PATCH] More: aligns the formalisation of de Bruijn indices with that in the previous chapter (#534) --- src/plfa/part2/More.lagda.md | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md index 6a46f4bb..06875843 100644 --- a/src/plfa/part2/More.lagda.md +++ b/src/plfa/part2/More.lagda.md @@ -558,8 +558,9 @@ and leave formalisation of the remaining constructs as an exercise. import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open import Data.Empty using (⊥; ⊥-elim) -open import Data.Nat using (ℕ; zero; suc; _*_) +open import Data.Nat using (ℕ; zero; suc; _*_; _<_; _≤?_; z≤n; s≤s) open import Relation.Nullary using (¬_) +open import Relation.Nullary.Decidable using (True; toWitness) ``` @@ -718,20 +719,24 @@ data _⊢_ : Context → Type → Set where ### Abbreviating de Bruijn indices ``` -lookup : Context → ℕ → Type -lookup (Γ , A) zero = A -lookup (Γ , _) (suc n) = lookup Γ n -lookup ∅ _ = ⊥-elim impossible - where postulate impossible : ⊥ +length : Context → ℕ +length ∅ = zero +length (Γ , _) = suc (length Γ) -count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n -count {Γ , _} zero = Z -count {Γ , _} (suc n) = S (count n) -count {∅} _ = ⊥-elim impossible - where postulate impossible : ⊥ +lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type +lookup {(_ , A)} {zero} (s≤s z≤n) = A +lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p -#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n -# n = ` count n +count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p +count {_ , _} {zero} (s≤s z≤n) = Z +count {Γ , _} {(suc n)} (s≤s p) = S (count p) + +#_ : ∀ {Γ} + → (n : ℕ) + → {n