Is there a way to tell Idris to interpret decimal strings such as 2, 10, etc as Nat? The default behavior in the repl is to interpret them as Integer. In Coq, for example, it's possible to specify an interpretation scope with % to disambiguate notations, so I guess I'm hoping that something like 10%Nat exists. Is there something like that in Idris?
The standard prelude contains
the : (a : Type) -> (value: a) -> a
the _ = id
which can be used to give explicit types:
the Integer 10
the Nat 6
the (Vect 3 Int) [1,2,3]
There's also with [namespace] [expr], which privileges namespace inside expr. This seems closer to %, but the seems more often used.
with Vect [['a', 'b']] -- Vect 1 (Vect 2 Char)
with List [['a', 'b']] -- List (List Char)
You can make a syntax extension for the:
syntax [expr] "%" [type] = the type expr
5%Nat
10%Int
But not for with.