Specify a scope for interpreting the decimal string as Nat

Question

Is there a way to tell Idris to interpret decimal strings like 2 , 10 , etc. how is Nat ? The default behavior in repl is to interpret them as Integer . For example, in Coq, you can specify the scope of interpretation with % to eliminate the ambiguity of the notation, so I think I hope that something like 10%Nat exists. Is there something similar in Idris?

Answer 1

The standard prelude contains

 the : (a : Type) -> (value: a) -> a the _ = id 

which can be used to provide explicit types:

 the Integer 10 the Nat 6 the (Vect 3 Int) [1,2,3] 

Here also with [namespace] [expr] , which grants namespace privileges inside expr . It seems closer to % , but the more commonly used.

 with Vect [['a', 'b']] -- Vect 1 (Vect 2 Char) with List [['a', 'b']] -- List (List Char) 

You can do the syntax extension for the :

 syntax [expr] "%" [type] = the type expr 5%Nat 10%Int 

But not for with .