Idris Nat letterali nei tipi

Question

Vorrei che Idris dimostrasse che lo testMult : mult 3 3 = 9 è abitato.

Purtroppo questo è tipizzata come

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

posso ovviare a questo modo:

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

C'è un modo per fare qualcosa che sarebbe simile a mult (3 : Nat) (3 : Nat) = (9 : Nat)?

Answer 1

È possibile utilizzare la funzione the : (a : Type) -> a -> a per specificare il tipo quando l'inferenza di tipo non riesce.

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

Si noti che è necessario avere the su entrambi i lati della uguaglianza perché Idris ha uguaglianza eterogeneo, cioè, (=) : {a : Type} -> {b : Type} -> a -> b -> Type.

In alternativa, si potrebbe scrivere

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

Se si preferisce quello stile.