------------------------------------------------------------------------
-- Normalisation
------------------------------------------------------------------------

module HOAS.SimplyTyped.Normalisation where

open import HOAS.SimplyTyped.TypeSystem
open import HOAS.SimplyTyped.NormalForm
open import HOAS.SimplyTyped.Value

-- Normalisation.

nf :  {τ}  Tm τ  NF τ
nf t = reify _  t