------------------------------------------------------------------------
-- Types used to make recursive arguments coinductive
------------------------------------------------------------------------

-- See Data.Colist for examples of how this type is used, or
-- http://article.gmane.org/gmane.comp.lang.agda/633 for a longer
-- explanation.

module Coinduction where

infix  ♯_ ♯₁_

codata ∞ (T : Set) : Set where
  ♯_ : (x : T) → ∞ T

♭ : ∀ {T} → ∞ T → T
♭ (♯ x) = x

-- Variant for Set₁.

codata ∞₁ (T : Set₁) : Set₁ where
  ♯₁_ : (x : T) → ∞₁ T

♭₁ : ∀ {T} → ∞₁ T → T
♭₁ (♯₁ x) = x