Agda-2.3.2.2: test/Common/Coinduction.agda

module Common.Coinduction where

open import Common.Level

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

private

  my-♯ : ∀ {a} {A : Set a} → A → ∞ A
  my-♯ x = ♯ x