module Core.Term.NormalForm

import Core.Context
import Core.Term
import Core.Var

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

public export
data Neutral : Term sx -> Type where
  Var : Neutral (Var v)

  App : Neutral t -> Neutral (App t u)

public export
data Whnf : Term sx -> Type where
  Ntrl : Neutral t -> Whnf t

  Set : Whnf Set

  Pi : Whnf (Pi n t u)
  Abs : Whnf (Abs n t)

%name Neutral n, m
%name Whnf n, m