Idris REPL：関数を作成する

Question

Idris REPLで関数を書くにはどうすればいいですか？私はREPLで関数定義​​を入力すると、私は次のエラーメッセージが表示されます：

(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コマンドを使用する必要があります。このように：あなたは、関数の種類を入力すると、イドリスREPLスマート何もしない

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

デフォルトでは、それはいくつかのスマートな複数行モードに入りません。 :letコマンドは、REPL内のトップレベルのバインディングを定義するために使用されます。

もう1つの瞬間：文字列型を使用する場合は、stringの代わりにString（大文字で始まる）を使用する必要があります。