Accéder à l'élément de Stream dans agda

J'ai créé un flux de type (N x N). Comment puis-je accéder à l'élément individuel de la paire ??Accéder à l'élément de Stream dans agda

genL : ℕ → Stream (ℕ × ℕ) → Stream (ℕ × ℕ) 
genL k ((x , y) :: xs) = if ((y * k) lt x) then (x , y) :: (♯ genL k (♭ xs)) 
          else genL k (♭ xs)

Il dit qu'il n'y a pas constuctor , en cours d'eau. J'ai une solution en tête que je vais créer des dossiers de paire alors ça va marcher. En dehors de cela, il existe un autre moyen d'accéder à l'élément.

Source

2015-03-31 ajayv

Êtes-vous à la recherche de [recherche] (http://agda.github.io/agda-stdlib/Data.Stream.html#2055)? Si non, pourriez-vous commencer par écrire le type de fonction que vous recherchez? – gallais

Non, le flux a un élément de la forme (x, y). Je veux accéder x et y séparément. Dans le code, la deuxième ligne ne fonctionne pas. – ajayv

Vous pouvez utiliser les [projections] de Data.Product (http://agda.github.io/agda-stdlib/Data.Product.html#525) pour cela. – gallais

Le constructeur est _∷_ (type \:: pour obtenir ∷), pas _::_.

De toute façon, votre définition n'est pas productive et ne convainc pas le vérificateur de terminaison.

Source

2015-04-01 06:24:45 user3237465

Non, le problème était avec ",". C'était typo i.e (: :). Comment convaincre le vérificateur de terminaison ?? C'est la raison pour laquelle j'ai placé NO_TERMINATION_CHECK. – ajayv

@ajayv, ce n'est pas clair ce que vous essayez d'atteindre. Il y avait un [chapitre] (http://adam.chlipala.net/cpdt/html/Coinductive.html) sur la coinduction dans le livre du CPDT. – user3237465

Accéder à l'élément de Stream dans agda

Répondre

Questions connexes