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

module SimplyTyped.Normalisation where

open import SimplyTyped.TypeSystem
open import SimplyTyped.NormalForm
open import SimplyTyped.ApplicativeStructure
open import SimplyTyped.Value
open ValSubst

-- Normalisation.

nf : ∀ {Γ τ} → Γ ⊢ τ → NF Γ τ
nf t = reify _ (⟦ t ⟧ idˢ)
  where open ApplicativeStructure appStr