Idris REPL: creating function

Question

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>
      ^

Answer 1

Idris documentation has example of what you need. You should use :let command. Like this:

Idris> :let longer : String -> String -> String; longer s1 s2 = if length s1 > length s2 then s1 else s2
Idris> longer "abacaba" "abracadabra"
"abracadabra" : String

By default Idris REPL doesn't do anything smart, it doesn't enter some smart multiline mode when you enter type of function. :let command is used to define any top-level bindings inside REPL.

Another moment: if you want to use string type you should use String (started with uppercase letter) instead of string.