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