From b6fb551360b283c38b3ede9ef3e6d2922bd62b58 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 12:00:01 +0000
Subject: Add the True type.

---
 src/Obs/Typing.idr | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src/Obs/Typing.idr')

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 ---------------------------------------------
 
-- 
cgit v1.2.3