Idris Natのリテラルタイプ

Question

IdrisはtestMult : mult 3 3 = 9に住人がいることを証明したいと思います。

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

mult (3 : Nat) (3 : Nat) = (9 : Nat)に類似して何かをする方法はあります：

残念ながら、これは

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

私はこのようにそれを回避することができますとして入力されましたか？

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 

を書くことができます。