[Agda] using literals and the standard library

[Martin Stone Davis]

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