{-# OPTIONS --universe-polymorphism #-} module PatternMatchingOnCodata where data Level : Set where zero : Level suc : (i : Level) → Level _⊔_ : Level → Level → Level zero ⊔ j = j suc i ⊔ zero = suc i suc i ⊔ suc j = suc (i ⊔ j) {-# BUILTIN LEVEL Level #-} {-# BUILTIN LEVELZERO zero #-} {-# BUILTIN LEVELSUC suc #-} {-# BUILTIN LEVELMAX _⊔_ #-} 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 ♭ #-} my-♭ : ∀ {a} {A : Set a} → ∞ A → A my-♭ (♯ x) = x