Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Idris Nat literals in types

Tags:

idris

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)?

like image 348
huynhjl Avatar asked Jul 25 '13 06:07

huynhjl


1 Answers

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.

like image 159
ReyCharles Avatar answered Oct 02 '22 00:10

ReyCharles