Idris REPL: Erstellen von Funktion

Question

Wie schreibe ich eine Funktion in der Idris REPL? Wenn ich die Funktionsdefinition longer: string -> string -> string in der REPL geben, erhalte ich die folgende Fehlermeldung:

(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 hat Beispiel dafür, was man braucht. Sie sollten den Befehl :let verwenden. Wie folgt aus:

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

standardmäßig Idris REPL tut nichts klug, es nicht einige intelligente mehrzeiligen Modus aufzurufen, wenn Sie Funktionstyp eingeben. Der Befehl :let wird verwendet, um Bindungen der obersten Ebene in REPL zu definieren.

Ein weiterer Moment: Wenn Sie String-Typ verwenden möchten, sollten Sie String (mit Großbuchstaben beginnen) anstelle von string verwenden.