module kleeneO  where


data ℕ : Set where
  Z : ℕ 
  S : ℕ -> ℕ


data O : Set where
  leaf : O
  succ : O -> O
  lim  : (ℕ -> O) -> O