{-# OPTIONS --safe #-}
open import Data.Nat.Base using (ℕ)
module Data.StagedTree (Item : ℕ → Set) where

open import Data.Nat.Base using (ℕ; zero; suc; _≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)

open import Data.StagedList using (StagedList)

-- A rose tree built from staged lists
infix  _⊢_
record StagedTree (n : ℕ) : Set where
  inductive
  constructor _⊢_
  field
    children : StagedList StagedTree n
    item : Item n

-- A forest is a list of trees
open import Data.StagedList StagedTree renaming (StagedList to StagedForest) public