类型中的 Idris Nat 文字

Question

我希望 Idris 证明 testMult : mult 3 3 = 9 有人居住。

不幸的是，这是键入为

mult (fromInteger 3) (fromInteger 3) = fromInteger 9 : Type

我可以这样解决它：

n3 : Nat; n3 = 3
n9 : Nat; n9 = 9
testMult : mult n3 n3 = n9
testMult = Refl

有没有办法做类似于mult (3 : Nat) (3 : Nat) = (9 : Nat) 的事情？

Answer 1

当类型推断失败时，您可以使用函数the : (a : Type) -> a -> a 指定类型。

testMult : the Nat (3 * 3) = the Nat 9
testMult = Refl

请注意，您需要在等式两边都有the，因为Idris 具有异构等式，即(=) : {a : Type} -> {b : Type} -> a -> b -> Type。

或者，你可以写

testMult : the Nat 3 * the Nat 3 = the Nat 9
testMult = Refl

如果你喜欢那种风格。