{-# OPTIONS --safe #-}
module Core.Context where

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

data Type : Set where
  _⇒_ : Type → Type → Type
  `Bool : Type
  ◯ : Type → Type

variable
  A B A′ B′ : Type

open import Data.StagedTree (λ _ → Type) renaming (StagedForest to Context; StagedTree to ContextItem) public

variable
  Γ Γ′ Δ Δ′ : Context n
  Γ₁ Γ₂ : Context n

infixl  _,_^_
pattern _,_^_ Γ A n = Γ ,[ ∅ ⊢ A ^ ≤‴-refl {m = n} ]