From ae80fe4d92ff37b3bdd1b9c34e277ec6c9d40eec Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sun, 16 Apr 2023 19:30:00 +0100 Subject: Define generic equality. Judgemental equality is a trivial instance. --- src/Core/Term/NormalForm.idr | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'src/Core/Term') 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) -- cgit v1.2.3