Idris Nat Literale in Typen

Question

Ich möchte Idris beweisen, dass testMult : mult 3 3 = 9 bewohnt ist.

Leider ist diese getippt als

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

Ich kann so um es:

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

Gibt es eine Möglichkeit, etwas zu tun, die mult (3 : Nat) (3 : Nat) = (9 : Nat) ähnlich sein würde?

Answer 1

Sie können die Funktion verwenden, um den Typ anzugeben, wenn die Typinferenz für Sie fehlschlägt.

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

Beachten Sie, dass the an beiden Seiten der Gleichung haben müssen, weil Idris heterogene Gleichheit hat, das heißt, (=) : {a : Type} -> {b : Type} -> a -> b -> Type.

Alternativ können Sie

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

schreiben Wenn Sie diesen Stil bevorzugen.