idris

8Hitze

4Antwort

Wo und warum sollte ich extra leere Muster verwenden?

Zum Beispiel: intersectBy : (a -> a -> Bool) -> List a -> List a -> List a intersectBy _ [] _ = [] intersectBy _ _ [] = [] intersectBy eq xs ys = [x | x <- xs, any (eq x) ys] Es gibt zusätzliche

9Hitze

1Antwort

Tell abhängige Funktion in bedingten Anweisung Zweig, die Bedingung ist wahr

Ich habe eine Funktion mit einem Typ Unterschrift (x, y : SomeType) -> (cond x y) = True -> SomeType. Wenn ich die Bedingung in if-then-else/case/with-Anweisung überprüfe, wie übertrage ich die Funkti

8Hitze

1Antwort

Postulate in Idris

Gibt es aktuelle Informationen über die Art und die Verwendung des postulate Konstrukts in Idris? Es gibt nichts zum Thema im Tutorial/Handbuch und ich kann auch nichts im Wiki finden. TIA.

5Hitze

1Antwort

Wartung eines Nat innerhalb eines festen Bereichs

Ich hätte gerne eine Nat, die innerhalb eines festen Bereichs bleibt. Ich möchte Funktionen incr und decr, die fehlschlagen, wenn sie die Zahl außerhalb des Bereichs schieben werden. Dies scheint, als

11Hitze

2Antwort

Verwenden benannte Instanzen für andere Instanzen

Ich versuche, eine Semigroup und VerifiedSemigroup Instanz auf meine benutzerdefinierten Bool Datentyp sowohl Betreiber ||&& und Betreiber zu machen: %case data Lógico = Cierto | Falso (&&) : Lógico

8Hitze

1Antwort

Einfache syntaktische Gleichheit in Idris

Gibt es eine einfache Möglichkeit, Gleichheit (DecEq) Instanzen für Datentypen zu schreiben? Zum Beispiel möchte ich die folgende O (n) Zeilen in seiner DecEq Erklärung zu haben, wo ?p ist etwas einfa

9Hitze

1Antwort

Wie kann ich einen Nummernkreis als Typ in Idris angeben?

Ich habe mit Idris experimentiert und es scheint wie es einfach sein sollte, eine Art von Typ für die Darstellung aller Zahlen zwischen zwei verschiedenen Zahlen, z. NumRange 5 10 ist der Typ aller Za

6Hitze

1Antwort

Idris: Nachweis, dass bestimmte Begriffe sind unmöglich

Idris Version: 0.9.16 I Konstruktionen aus einem base Wert und einer iterierten step Funktion erzeugt, zu beschreiben versucht bin: namespace Iterate data Iterate : (base : a) -> (step : a -> a)

18Hitze

1Antwort

Bibliothek generieren statt ausführbar in Idris?

Gibt es eine Möglichkeit, eine Bibliothek anstelle einer ausführbaren Datei mit idris zu generieren? Wenn ich ohne main versuchen kompilieren, ich einen Fehler wie diese: main:0:0:When elaborating an

5Hitze

2Antwort

In Idris, wie schreibe ich eine "vect Generator" -Funktion, die eine Funktion des Index in Parameter

Ich versuche, in Idris eine Funktion zu schreiben, die ein Vect durch die Größe des Vect und eine Funktion, die den Index zu übergeben in Parameter. Bisher habe ich dies: import Data.Fin import Data.