diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 6 |
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 --------------------------------------------- |