open import Agda.Builtin.Nat using (Nat; suc)

-- ** functions

@0 erasedFun : Nat → Nat
erasedFun x = x

module @0 ErasedModule where postulate
  _≡_ : Nat → Nat → Set
  _≤_ : Nat → Nat → Set
open ErasedModule

erasedFunArg : (n : Nat) → @0 (n ≡ ) → Nat
erasedFunArg n _ = suc n

erasedHigherOrderFunArg : @0 Nat → (@0 Nat → Nat) → Nat
erasedHigherOrderFunArg n f = suc (f n)

-- ** records

record @ ErasedRec (x y : Nat) : Set where
  field x≡y : x ≡ y

erasedRec : {@0 x y : Nat} → @0 ErasedRec x y → Nat
erasedRec _ = 

record ErasedField : Set where
  field x : Nat
        @0 x≡0 : x ≡ 

succ : ErasedField → Nat
succ (record {x = x}) = suc x

record ErasedRecParam (@0 x : Nat) : Set where
  field y : Nat
        @0 x≡y : x ≡ y

erasedRecParam : (@0 x : Nat) → ErasedRecParam x → Nat
erasedRecParam _ (record {y = y}) = y

erasedRecParamH : {@0 x : Nat} → ErasedRecParam x → Nat
erasedRecParamH (record {y = y}) = y

-- ** datatypes

data @ ErasedData : Set where
  mk : (m n : Nat) → m ≡ n → ErasedData

erasedData : @0 ErasedData → Nat
erasedData (mk m n _) = 

data ErasedCon : Set where
  mk : Nat → ErasedCon
  @0 mkIrr : (m : Nat) → m ≡  → ErasedCon

erasedClause : ErasedCon → Nat
erasedClause (mk n) = n
erasedClause (mkIrr n _) = n

data ErasedConArg : Set where
  mk : (n : Nat) → @0 (n ≡ ) → ErasedConArg

erasedConArg : ErasedConArg → Nat
erasedConArg (mk n _) = n

data BST (@0 lower upper : Nat) : Set where
  Leaf : (@0 pf : lower ≤ upper) → BST lower upper
  Node : (x : Nat) (l : BST lower x) (r : BST x upper) → BST lower upper

open import Agda.Builtin.Nat

postulate
  refl   : ∀ {n} → n ≡ n
  ≤-refl : ∀ {n} → n ≤ n

sumBST : ∀ {n m} → BST n m → Nat
sumBST = λ where
  (Leaf _) → 
  (Node n t t′) → n + sumBST t + sumBST t′

test : Nat
test = (erasedFunArg  refl + erasedHigherOrderFunArg  (λ _ → ))
     + erasedRec (record { x≡y = refl {} })
     + (succ (record { x =  ; x≡0 = refl }) + )
     + erasedRecParam _ (record { y =  ; x≡y = refl })
     + erasedRecParamH (record { y =  ; x≡y = refl })
     + erasedData (mk  _ refl)
     + (erasedClause (mk ) + erasedConArg (mk  refl))
     + sumBST (Node  (Leaf ≤-refl) (Node  (Leaf ≤-refl) (Leaf ≤-refl)))
{-# COMPILE AGDA2LAMBOX test #-}