agda-unused-0.1.0: data/Agda/Builtin/Coinduction.agda

{-# OPTIONS --without-K --safe --universe-polymorphism --no-sized-types
            --no-guardedness --no-subtyping #-}

module Agda.Builtin.Coinduction where

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     ♭  #-}