1 files changed, 11 insertions, 0 deletions
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 97a0d48..f930176 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -18,6 +18,7 @@ data NormalForm  : Nat -> Type
 public export
 data Constructor : Nat -> Type where
   Sort : Sort -> Constructor n
+  Top  : Constructor n
 
 public export
 data Neutral : Nat -> Type where
@@ -27,6 +28,7 @@ public export
 data NormalForm : Nat -> Type where
   Ntrl  : Neutral n -> NormalForm n
   Cnstr : Constructor n -> NormalForm n
+  Irrel : NormalForm n
 
 public export
 record Definition (n : Nat) where
@@ -49,11 +51,14 @@ eqNtrl  : Neutral n -> Neutral n -> Bool
 eqWhnf  : NormalForm n -> NormalForm n -> Bool
 
 eqCnstr (Sort s) (Sort s') = s == s'
+eqCnstr Top      Top       = True
+eqCnstr _ _ = False
 
 eqNtrl (Var i) (Var j) = i == j
 
 eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
 eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
+eqWhnf Irrel     Irrel     = True
 eqWhnf _ _ = False
 
 export
@@ -75,11 +80,13 @@ prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
 prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
 
 prettyPrecCnstr d (Sort s) = prettyPrec d s
+prettyPrecCnstr d Top = pretty "()"
 
 prettyPrecNtrl d (Var i) = pretty "$\{show i}"
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
 prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
+prettyPrecWhnf d Irrel     = pretty "_"
 
 export
 Pretty (Constructor n) where
@@ -114,11 +121,13 @@ renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
 renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 
 renameCnstr (Sort s) f = Sort s
+renameCnstr Top      f = Top
 
 renameNtrl (Var i) f = Var (f i)
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
 renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
+renameWhnf Irrel     f = Irrel
 
 export
 Rename Constructor where
@@ -139,11 +148,13 @@ substNtrl  : Neutral n -> (Fin n -> NormalForm m) -> NormalForm m
 substWhnf  : NormalForm n -> (Fin n -> NormalForm m) -> NormalForm m
 
 substCnstr (Sort s) f = Sort s
+substCnstr Top      f = Top
 
 substNtrl (Var i) f = f i
 
 substWhnf (Ntrl t)  f = substNtrl t f
 substWhnf (Cnstr t) f = Cnstr $ substCnstr t f
+substWhnf Irrel     f = Irrel
 
 export
 Subst Constructor NormalForm Constructor where