{-# 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