Idris REPL：创建函数

Question

如何在 Idris REPL 中编写函数？如果我在 REPL 中键入函数定义 longer: string -> string -> string，我会收到以下错误消息：

(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 有您需要的示例。您应该使用:let 命令。像这样：

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

默认情况下，Idris REPL 不会做任何智能操作，当您输入函数类型时，它不会进入一些智能多行模式。 :let 命令用于定义 REPL 中的任何顶级绑定。

另一个时刻：如果你想使用字符串类型，你应该使用String（以大写字母开头）而不是string。