伊德里斯納特文字類型

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在平等的雙方，因爲伊德里斯具有異質性的平等，也就是(=) : {a : Type} -> {b : Type} -> a -> b -> Type。

或者，如果你喜歡這種風格，你可以寫

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

。