[Agda] Resolving a universe level problem

[Marko Dimjašević]

Dear Jesper,

On Wed, 2020-09-09 at 09:12 +0200, Jesper Cockx wrote:
> 
> Here Agda is complaining that you gave it a type (something of type
> `Set`), but it expected something of type `suc n Nat.≤ Context-size Γ`.
> Indeed, you gave `n < Context-size Γ` in the type of #'_, but you
> should've given a *proof* of that type. One way to fix the problem is by
> adding an extra argument of this type to the function `#'_`. By adding an
> argument of this type, you make explicit the precondition that the number
> `n` should not be greater than the length of the context, which was
> implicit in the plfa version.


Jesper, thank you a lot for pointing this out! You're right, I confused a
theorem for a proof.

This got it working:

#'_ : ∀ {Γ} → (n : ℕ) → {s : suc n ≤? (Context-size Γ)} → Γ ⊢ lookup' Γ n
(soundness-< n (Context-size Γ) s)
#'_ {Γ} n {s}  =  ` count' n (soundness-< n (Context-size Γ) s)


Now #'_ can be used the same way as #_ without making the user provide an
explicit within-context-bounds proof.


--
Kind regards,
Marko

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200909/00a76dca/attachment.sig>