Idris Nat文字类型

Question

我想伊德里斯证明这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

如果你喜欢那种风格.