idris - 型内の 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

theIdris には異種の等式、つまり があるため、等式の両側にある必要があることに注意してください(=) : {a : Type} -> {b : Type} -> a -> b -> Type。

または、次のように書くこともできます

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

あなたがそのスタイルを好むなら。