module Record.Annotatability.Target where

open import Record.Prelude
open import Record.PreCommon

infixr 5  ฦ›_
infixl 7  _ยท_
infix  9  `_
infix  2 ๐•ฃ_
infixr 5 rโŸฆ_โ†ฆ_โŸง_


data Term : Set
data Record : Set

data Term where
  ๐•”_       : Constant โ†’ Term
  `_       : โ„• โ†’ Term
  ฦ›_       : Term โ†’ Term
  _ยท_      : Term โ†’ Term โ†’ Term
--  _โฆ‚_      : Term โ†’ Type โ†’ Term
  ๐•ฃ_       : Record โ†’ Term
  _๐•ก_      : Term โ†’ Label โ†’ Term

data Record where
  rnil : Record
  rโŸฆ_โ†ฆ_โŸง_ : Label โ†’ Term โ†’ Record โ†’ Record