I'd like Idris to prove that testMult : mult 3 3 = 9
is inhabited.
Unfortunately this is typed as
mult (fromInteger 3) (fromInteger 3) = fromInteger 9 : Type
I can work around it like this:
n3 : Nat; n3 = 3
n9 : Nat; n9 = 9
testMult : mult n3 n3 = n9
testMult = Refl
Is there a way to do something that would be similar to mult (3 : Nat) (3 : Nat) = (9 : Nat)
?
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With