module Orn.Reornament.Examples.Maybe (A : Set) where open import Data.Unit open import Data.Product open import IDesc.Fixpoint open import IDesc.Examples.Bool open import Orn.Ornament open import Orn.Ornament.Examples.Maybe open import Orn.Reornament -- Paper: Example 4.31 iMaybe : Bool → Set iMaybe b = μ ⌈ MaybeO A ⌉D (tt , b) inothing : iMaybe false inothing = ⟨ tt ⟩ ijust : A → iMaybe true ijust a = ⟨ a , tt ⟩