1
{-# OPTIONS --guardedness-preserving-type-constructors #-}
10
_⊔_ : Level → Level → Level
12
{-# BUILTIN LEVEL Level #-}
13
{-# BUILTIN LEVELZERO zero #-}
14
{-# BUILTIN LEVELSUC suc #-}
15
{-# BUILTIN LEVELMAX _⊔_ #-}
20
∞ : ∀ {a} (A : Set a) → Set a
21
♯_ : ∀ {a} {A : Set a} → A → ∞ A
22
♭ : ∀ {a} {A : Set a} → ∞ A → A
24
{-# BUILTIN INFINITY ∞ #-}
25
{-# BUILTIN SHARP ♯_ #-}
26
{-# BUILTIN FLAT ♭ #-}
28
data CoNat : Set0 where
36
record B (a : ∞ A) : Set1 where
b'\\ No newline at end of file'