[Agda] using literals and the standard library

[Guillaume Allais]

I meant not importing anything unit-related.
I don't get any error (using either 2.5.4.2 or 2.6.0-329b843) with:

```
open import Agda.Builtin.FromNat
open import Data.Nat
open import Data.Nat.Literals
open import Data.Fin
open import Data.Fin.Literals

instance
  _ = Data.Nat.Literals.number
  _ = Data.Fin.Literals.number

test-nat : ℕ
test-nat = 3

test-fin : Fin 7
test-fin = 3
```


On 06/12/2018 01:58, Martin Stone Davis wrote:
> Hi Guillaume,
>
> I'm not sure what you meant by your remark that it's not necessary to import
> Data.Unit. Did you just mean that it could be replaced with an import of
> Agda.Builtin.Unit? If you meant that it could simply be removed, know that,
> without that import, I get the following error in `test-nat`:
>
> ```
> No instance of type ;Agda.Builtin.Unit.⊤ was found in scope.
> when checking that 3 is a valid argument to a function of type
> {a : ;Agda.Primitive.Level} {A : Set a} ⦃ r : Number A ⦄ (n : ℕ)
> ⦃ _ : r .Number.Constraint n ⦄ →
> A
> ```
>
> -M
>
>
> On 12/05/2018 12:04 PM, Guillaume Allais wrote:
>> 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/20181206/35e9788a/attachment.sig>