You can use the function the : (a : Type) -> a -> a
to specify the type when the type inference is failing for you.
testMult : the Nat (3 * 3) = the Nat 9
testMult = Refl
Note that you need to have the
at both sides of the equality because Idris has heterogenous equality, that is, (=) : {a : Type} -> {b : Type} -> a -> b -> Type
.
Alternatively, you could write
testMult : the Nat 3 * the Nat 3 = the Nat 9
testMult = Refl
If you prefer that style.