module Core.Term

import public Data.Fin

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

public export
data Term : Nat -> Type where
  Var : Fin n -> Term n

  Set : Term n

  Pi : Term n -> Term (S n) -> Term n
  Abs : Term (S n) -> Term n
  App : Term n -> Term n -> Term n

%name Term t, u, v