Add the True type.

1 files changed, 5 insertions, 1 deletions

diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 95ffc19..22994ec 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -20,11 +20,13 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 -- invariant: all definitions fully expanded
 -- invariant: m |- t, u <- a : s
 convert : (t, u, a : NormalForm n) -> Sort -> Bool
-convert t u a Prop = True
+convert Irrel Irrel a Prop = True
 convert t u (Ntrl _) (Set k) = t == u
+convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort Prop)) (Set 0) = True
 convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = Ntrl t == u
 convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = t == Ntrl u
 convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort s)) (Set k) = s' == s''
+convert _ _ _ _ = False
 
 -- Typing Contexts -------------------------------------------------------------
 
@@ -71,6 +73,8 @@ check ctx tm ty s = do
 
 infer ctx (Var b i) = pure $ index ctx i
 infer ctx (Sort b s) = pure $ (Cnstr (Sort s), Cnstr (Sort (suc s)), suc (suc s))
+infer ctx (Top b) = pure $ (Cnstr Top, Cnstr (Sort Prop), Set 0)
+infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
 
 -- Checking Definitions and Blocks ---------------------------------------------