[Made the return constructor superfluous by switching from data to codata.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080703174446] hunk ./Infinite.agda 138
--- to a more dependently typed setting, and made it possible to map
--- over the resulting values without having to manipulate the seed.
+-- to a more dependently typed setting, made it possible to map over
+-- the resulting values without having to manipulate the seed, and
+-- made the return constructor superfluous by switching to a
+-- coinductive type for right-hand sides.
hunk ./Infinite.agda 147
-data Infiniteʳ {I S : Set} (R : I -> Rel S) (P : I -> Pred S) :
-               Guardedness -> I -> S -> Set where
-  return : forall {g i x} (x⟶∞ : Infinite (R i) x) ->
-           Infiniteʳ R P g i x
+codata Infiniteʳ {I S : Set} (R : I -> Rel S) (P : I -> Pred S) :
+                 Guardedness -> I -> S -> Set where
hunk ./Infinite.agda 155
+return : forall {I S R g i x} {P : I -> Pred S} ->
+         Infinite (R i) x -> Infiniteʳ R P g i x
+return (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ return y⟶∞
+
hunk ./Infinite.agda 166
-map∞ʳ F f (return x⟶∞)   = return (map∞ F f x⟶∞)
-map∞ʳ F f (x⟶y ◅∞ y⟶∞)   = f x⟶y ◅∞ map∞ʳ F f y⟶∞
-map∞ʳ F f (grec F' f' p) = grec (F ∘ F') (f ∘ f') p
+map∞ʳ F f (x⟶y ◅∞ y⟶∞)   ~ f x⟶y ◅∞ map∞ʳ F f y⟶∞
+map∞ʳ F f (grec F' f' p) ~ grec (F ∘ F') (f ∘ f') p
hunk ./Infinite.agda 177
-unfold1 step (return x⟶∞) = return x⟶∞
hunk ./Infinite.agda 184
-produce step (return x⟶∞) ~ x⟶∞
hunk ./Infinite.agda 200
-weaken (return x⟶∞) = return x⟶∞