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 함수를 사용하여 유형을 지정할 수 있습니다. 당신이 이드리스는 이종 평등을 가지고 있기 때문에 평등의 양쪽에 the이 필요

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

주, 즉, (=) : {a : Type} -> {b : Type} -> a -> b -> Type입니다. 당신이 스타일을 선호하는 경우

또는,

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

을 작성할 수 있습니다.