Some typing rule commentsHEADmaster

1 files changed, 20 insertions, 0 deletions

diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs
index 6777ec8..bc25419 100644
--- a/src/TypeCheck.hs
+++ b/src/TypeCheck.hs
@@ -97,17 +97,37 @@ inferW env term = do
 
 infer :: Env -> Term -> TM (OfType Term Term)
 infer env = \case
+  -- Γ |- t ~~> τ       -- this is infer, dropping the term result (don't need that)
+  -- τ ~WHNF~> τ'
+  -- ----
+  -- Γ |- t ~~>_W τ'
+
+
+  -- ----
+  -- Set i : Set (isucc i)
   TSet i -> do
     return (TSet i :| TSet (TISucc i))
 
+  -- ----
+  -- Setω i : Setω (i + 1)
   TSetw i -> do
     return (TSetw i :| TSetw (succ i))
 
+  -- x : τ \in Γ
+  -- ----
+  -- Γ |- x : τ
   TVar n -> do
     case Map.lookup n env of
       Just (_ :| ty) -> return (TVar n :| ty)
       Nothing -> throw $ "Variable out of scope: " ++ n
 
+  -- Γ |- a ~~>_W τ₁
+  -- Γ, x : a |- b ~~>_W τ₂
+  -- k₁ <- ArgKind(τ₁)
+  -- k₂ <- ArgKind(τ₂)
+  -- τ <- ArgKindLower(k₁ <> k₂)
+  -- ----
+  -- Γ |- Π (x : a) b : τ
   TPi x a b -> do
     inferW env a >>= \case
       a' :| (argumentKind -> Just kindA) -> do