More: align the names of parameters to #_ to those in Chapter DeBruijn (#543)
This commit is contained in:
parent
a9ecf866c2
commit
95b39edde5
1 changed files with 4 additions and 4 deletions
|
@ -733,10 +733,10 @@ 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)
|
||||
→ {n∈Γ : True (suc n ≤? length Γ)}
|
||||
--------------------------------
|
||||
→ Γ ⊢ lookup (toWitness n∈Γ)
|
||||
#_ n {n∈Γ} = ` count (toWitness n∈Γ)
|
||||
```
|
||||
|
||||
## Renaming
|
||||
|
|
Loading…
Reference in a new issue