------------------------------------------------------------------------
-- 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 ⟧