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