[Agda] using literals and the standard library

[Guillaume Allais]

Hi Martin,

That looks like a reasonable module definition (with the side remark
that it's not necessary to import Data.Unit).

We are a bit reluctant to add instance declarations to the standard
library because they can't be hidden upon module import so users would
necessarily have them in scope even if they don't want them.

As for the Data.Fin.Literals.number if we do need the natural number
to be implicit for it to be usable directly as an instance, I think
that should indeed be modified in the stdlib.

Cheers,
--
gallais


On 05/12/2018 06:31, Martin Stone Davis wrote:
> To get both Nat and Fin literals using the standard library (latest development
> versions, including Jesper's latest re: instance resolution), I write the
> following:
> 
> ```agda
> open import Agda.Builtin.FromNat
> open import Data.Nat
> open import Data.Nat.Literals
> open import Data.Fin
> open import Data.Fin.Literals
> open import Data.Unit -- or Agda.Builtin.Unit
> 
> instance
>   _ = Data.Nat.Literals.number
> 
>   _ : ∀ {n} → Number (Fin n)
>   _ = Data.Fin.Literals.number _
> 
> test-nat : ℕ
> test-nat = 3
> 
> test-fin : Fin 7
> test-fin = 3
> ```
> 
> It's a bit annoying to need to import from Agda.Builtin.FromNat and from
> Data.Unit, so I wonder if this is the recommended approach? Also, should
> Data.Fin.Literals.number be updated to take a hidden argument (given that the
> new instance resolution does not count explicit arguments as instance arguments
> anymore)?
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181205/e0ded698/attachment.sig>