From 3eb03e2347b35432f7eae7d6847ec9ecf1dff19e Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 1 Jun 2023 11:54:49 +0100 Subject: Define terms with substitution as an operation. --- src/Total/NormalForm.idr | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 src/Total/NormalForm.idr (limited to 'src/Total/NormalForm.idr') diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr new file mode 100644 index 0000000..7421ca9 --- /dev/null +++ b/src/Total/NormalForm.idr @@ -0,0 +1,31 @@ +module Total.NormalForm + +import Total.Reduction +import Total.Term + +public export +data Neutral : Term ctx ty -> Type +public export +data Normal : Term ctx ty -> Type + +data Neutral where + Var : Neutral (Var i) + App : Neutral t -> Normal u -> Neutral (App t u) + Rec : Neutral t -> Normal u -> Normal v -> Neutral (Rec t u v) + +data Normal where + Ntrl : Neutral t -> Normal t + Abs : Normal t -> Normal (Abs t) + Zero : Normal Zero + Suc : Normal t -> Normal (Suc t) + +%name Neutral n, m, k +%name Normal n, m, k + +record NormalForm (0 t : Term ctx ty) where + constructor MkNf + term : Term ctx ty + 0 steps : t >= term + 0 normal : Normal term + +%name NormalForm nf -- cgit v1.2.3