{-# 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 4 _⊢_
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