Define generic equality.

Judgemental equality is a trivial instance.

1 files changed, 23 insertions, 0 deletions

diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr
index 9984bee..2cd16a1 100644
--- a/src/Core/Term/NormalForm.idr
+++ b/src/Core/Term/NormalForm.idr
@@ -1,6 +1,9 @@
 module Core.Term.NormalForm
 
 import Core.Term
+import Core.Thinning
+
+import public Data.DPair
 
 -- Definition ------------------------------------------------------------------
 
@@ -20,3 +23,23 @@ data Whnf : Term n -> Type where
 
 %name Neutral n, m
 %name Whnf n, m
+
+public export
+NeutralTerm : Nat -> Type
+NeutralTerm n = Subset (Term n) Neutral
+
+-- Inversion -------------------------------------------------------------------
+
+invertNtrlApp : Neutral (App t u) -> Neutral t
+invertNtrlApp (App n) = n
+
+-- Weakening -------------------------------------------------------------------
+
+export
+wknPresNtrl : Neutral t -> (thin : m `Thins` n) -> Neutral (wkn t thin)
+wknPresNtrl Var thin = Var
+wknPresNtrl (App n) thin = App (wknPresNtrl n thin)
+
+public export
+wkn : NeutralTerm m -> m `Thins` n -> NeutralTerm n
+wkn (Element t n) thin = Element (wkn t thin) (wknPresNtrl n thin)