[Agda] Overloaded literals

[Nils Anders Danielsson]

On 2011-06-27 08:37, Dominique Devriese wrote:
> My design is based on the following type class:
>
>    record HasNatLiterals (t : Set) : Set₁ where
>      field ValidLiteral : ℕ → Set
> 	  decideValid : (n : ℕ) → Dec (ValidLiteral n)
> 	  fromℕ : (n : ℕ) → {valid : True (decideValid n)} → t

Do you use BUILTIN pragmas to "bless" this type?

>    wnlFin : {k : ℕ} → HasNatLiterals (Fin k)
>    wnlFin {k} = record { ValidLiteral = λ n → n<  k;
> 			 decideValid = λ n → suc n ≤? k;
> 			 fromℕ = fromℕ′ }
> 	  where fromℕ′ : (n : ℕ) → {valid : True (suc n ≤? k)} → Fin k
> 		fromℕ′ n {valid} with suc n ≤? k
> 		fromℕ′ n {tt} | yes n<k = fromℕ≤ n<k
> 		fromℕ′ n {} | no ¬n<k

fromℕ′ is available (more or less) in the standard library as
Data.Fin.#_. The following code is accepted:

   i : Fin 1000
   i = # 2

With your suggested feature we can write the following instead:

>    test₂′ : Fin 1000
>    test₂′ = 2
>      where wnl = wnlFin

The difference seems small to me. Do you have a killer application in
mind?

-- 
/NAD