More: aligns the formalisation of de Bruijn indices with that in the previous chapter (#534)

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
+length : Context → ℕ
-lookup (Γ , A) zero     =  A
+length ∅        =  zero
-lookup (Γ , _) (suc n)  =  lookup Γ n
+length (Γ , _)  =  suc (length Γ)
-lookup ∅       _        =  ⊥-elim impossible
-  where postulate impossible : ⊥
 
-count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
+lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type
-count {Γ , _} zero     =  Z
+lookup {(_ , A)} {zero}    (s≤s z≤n)  =  A
-count {Γ , _} (suc n)  =  S (count n)
+lookup {(Γ , _)} {(suc n)} (s≤s p)    =  lookup p
-count {∅}     _        =  ⊥-elim impossible
-  where postulate impossible : ⊥
 
-#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
+count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p
-# n  =  ` count n
+count {_ , _} {zero}    (s≤s z≤n)  =  Z
+count {Γ , _} {(suc n)} (s≤s p)    =  S (count p)
+
+#_ : ∀ {Γ}
+  → (n : ℕ)
+  → {n<?length : True (suc n ≤? length Γ)}
+    --------------------------------------
+  → Γ ⊢ lookup (toWitness n<?length)
+#_ n {n<?length}  =  ` count (toWitness n<?length)
 ```
 
 ## Renaming