Write an encoding for data types.

1 files changed, 0 insertions, 51 deletions

diff --git a/src/NormalForm.idr b/src/NormalForm.idr
deleted file mode 100644
index ea3b2c0..0000000
--- a/src/NormalForm.idr
+++ /dev/null
@@ -1,51 +0,0 @@
-module NormalForm
-
-import Data.SnocList.Elem
-import Term
-import Thinning
-
--- Neutrals and Normals --------------------------------------------------------
-
-public export
-data IsNeutral : Term ctx ty -> Type
-public export
-data IsNormal : Term ctx ty -> Type
-
-data IsNeutral where
-  Var : IsNeutral (Var i)
-  App : IsNeutral t -> IsNormal u -> IsNeutral (App t u)
-  Rec : IsNeutral t -> IsNormal u -> IsNormal v -> IsNeutral (Rec t u v)
-
-data IsNormal where
-  Ntrl : IsNeutral t -> IsNormal t
-  Abs : IsNormal t -> IsNormal (Abs t)
-  Zero : IsNormal Zero
-  Succ : IsNormal t -> IsNormal (Succ t)
-
-%name IsNeutral prf
-%name IsNormal prf
-
-public export
-record Normal (ctx : SnocList Ty) (ty : Ty) where
-  constructor MkNormal
-  forget : Term ctx ty
-  0 isNormal : IsNormal forget
-
-%name Normal n, m, k
-
--- Inversions ------------------------------------------------------------------
-
-export
-Uninhabited (IsNormal (Sub t sub)) where uninhabited (Ntrl prf) impossible
-
-export
-predNorm : IsNormal (Succ t) -> IsNormal t
-predNorm (Succ prf) = prf
-
-export
-appNtrl : IsNormal (App t u) -> IsNeutral (App t u)
-appNtrl (Ntrl prf) = prf
-
-export
-recNtrl : IsNormal (Rec t u v) -> IsNeutral (Rec t u v)
-recNtrl (Ntrl prf) = prf