I can easily rewrite 01-Arithmetic.idr so that all the booleans are True and there are no metavariables, but is that the intent of the exercise? Should I instead try to write definitions for the "holes"?
Type checking ./01-Arithmetic.idr
Metavariables: Koans.Arithmetic.fillme5, Koans.Arithmetic.fillme4, Koans.Arithmetic.fillme3, Koans.Arithmetic.fillme2, ... ( + 1 other)
*01-Arithmetic> :t Koans.Arithmetic.fillme1
a : Type
class : Eq Integer
class1 : Num Integer
--------------------------------------
Koans.Arithmetic.fillme1 : Integer
It appears to be an Integer. But I can't simply assign an integer value to it and recompile the function, can I?
*01-Arithmetic> Koans.Arithmetic.fillme1 = 40
Can't resolve type class Num (Type -> Eq Integer -> Num Integer -> Integer)
Metavariables: Koans.Arithmetic.fillme5, Koans.Arithmetic.fillme4, Koans.Arithmetic.fillme3, Koans.Arithmetic.fillme2, ... ( + 1 other)
I gather now that I really should just fill in the blanks directly and see if the file compiles. But I thought I'd open this issue in case knowing an area where I got confused would be helpful in future efforts.