Idris REPL:创建函数
Idris REPL: creating function
如何在 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>
^
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
。
如何在 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>
^
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
。