Idris REPL: creating function

Viewed 650

How do I write a function in the Idris REPL ? If I type the function definition longer: string -> string -> string in the REPL, I get the following error message :

(input):1:7: error: expected: "$",
    "&&", "*", "*>", "+", "++", "-",
    "->", ".", "/", "/=", "::", "<",
    "<$>", "<*", "<*>", "<+>", "<<",
    "<=", "<==", "<|>", "=", "==",
    ">", ">=", ">>", ">>=", "\\\\",
    "`", "|", "||", "~=~",
    ambiguous use of a left-associative operator,
    ambiguous use of a non-associative operator,
    ambiguous use of a right-associative operator,
    end of input, function argument
longer: string -> string -> string<EOF>
      ^
1 Answers
Related