Idris Nat literals theo loại

Question

Tôi muốn Idris chứng minh rằng testMult : mult 3 3 = 9 là nơi sinh sống.

Đáng tiếc là điều này được đánh máy như

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

tôi có thể làm việc xung quanh nó như thế này:

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

Có cách nào để làm điều gì đó mà có thể tương tự như mult (3 : Nat) (3 : Nat) = (9 : Nat)?

Answer 1

Bạn có thể sử dụng hàm the : (a : Type) -> a -> a để chỉ định loại khi suy luận loại không thành công cho bạn.

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

Lưu ý rằng bạn cần phải có the ở cả hai bên của bình đẳng vì Idris có bình đẳng heterogenous, có nghĩa là, (=) : {a : Type} -> {b : Type} -> a -> b -> Type.

Ngoài ra, bạn có thể viết

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

Nếu bạn thích phong cách đó.