Literały Idris Nat w typach

Question

Chciałbym, aby Idris udowodnił, że testMult : mult 3 3 = 9 jest zamieszkany.

Niestety to jest wpisane jako

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

można obejść to tak:

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

Czy istnieje sposób, aby zrobić coś, co byłoby podobne do mult (3 : Nat) (3 : Nat) = (9 : Nat)?

Answer 1

Możesz użyć funkcji the : (a : Type) -> a -> a, aby określić typ, gdy wnioskowanie o typ nie działa.

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

Pamiętaj, że musisz mieć the po obu stronach równości ponieważ Idris ma niejednorodną równości, czyli (=) : {a : Type} -> {b : Type} -> a -> b -> Type.

Alternatywnie, można napisać

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

Jeśli wolisz styl.