idris-hackers / idris-koans Goto Github PK

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

When I opened idris 01-Arithmetic.idr originally, the repl said there were several "Metavariables".

Type checking ./01-Arithmetic.idr
Metavariables: Koans.Arithmetic.fillme5, Koans.Arithmetic.fillme4, Koans.Arithmetic.fillme3, Koans.Arithmetic.fillme2, ... ( + 1 other)

I thought maybe I should provide a value for fillme1, so I inquired after its type:

*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.