1
{-# OPTIONS --universe-polymorphism #-}
3
module Imports.Coinduction where
5
open import Imports.Level
10
∞ : ∀ {a} (A : Set a) → Set a
11
♯_ : ∀ {a} {A : Set a} → A → ∞ A
12
♭ : ∀ {a} {A : Set a} → ∞ A → A
14
{-# BUILTIN INFINITY ∞ #-}
15
{-# BUILTIN SHARP ♯_ #-}
16
{-# BUILTIN FLAT ♭ #-}