De Bruijn: fixes alignment of arguments to #_ (#535)

This commit is contained in:
Marko Dimjašević 2020-10-24 16:59:43 +02:00 committed by GitHub
parent 51cd3fb64a
commit 5326f16a8b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -444,10 +444,10 @@ count {Γ , _} {(suc n)} (s≤s p) = S (count p)
We can then introduce a convenient abbreviation for variables:
```
#_ : ∀ {Γ}
→ (n : )
→ {n∈Γ : True (suc n ≤? length Γ)}
--------------------------------
→ Γ ⊢ lookup (toWitness n∈Γ)
→ (n : )
→ {n∈Γ : True (suc n ≤? length Γ)}
--------------------------------
→ Γ ⊢ lookup (toWitness n∈Γ)
#_ n {n∈Γ} = ` count (toWitness n∈Γ)
```
Function `#_` takes an implicit argument `n∈Γ` that provides evidence for `n` to