module Core.Term

import Core.Context
import Core.Var

%prefix_record_projections off

-- Definition ------------------------------------------------------------------

public export
data Term : Context -> Type where
  Var : Var sx -> Term sx

  Set : Term sx

  Pi : (n : Name) -> Term sx -> Term (sx :< n) -> Term sx
  Abs : (n : Name) -> Term (sx :< n) -> Term sx
  App : Term sx -> Term sx -> Term sx

%name Term t, u, v