指定解释范围以将十进制字符串解释为 Nat

Question

有没有办法告诉伊德里斯将十进制字符串如2、10等解释为Nat？repl 中的默认行为是将它们解释为 Integer 。例如，在 Coq 中，可以使用%指定解释范围以消除符号的歧义，所以我想我希望存在类似10%Nat的东西。伊德里斯有这样的事情吗？

Answer 1

标准前奏包含

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

可用于提供显式类型：

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

还有with [namespace] [expr]，expr内部namespace特权。这似乎更接近%，但the似乎更常用。

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

您可以为the进行语法扩展：

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

但不适合with.