checkpoint before FC

newt/testcase.newt

@@ -15,7 +15,9 @@ plus = \ n m => case n of
   Z => m
   S k => S (plus k m)
 
+-- So this isn't working at the moment, I think I need
+-- to replace the n with S ?k
 length : {a : U} {n : Nat} -> Vect n a -> Nat
 length = \ v => case v of
   Nil => Z
-  Cons x xs => S (length {a} xs)
+  Cons {a} {n'} x xs => S (length {a} xs)

src/Lib/Check.idr

@@ -210,6 +210,11 @@ checkAlt scty ctx ty (MkAlt ptm body) = do
       let var = VVar (length ctx.env) [<]
       let ctx' = extend ctx nm a
       Lam nm <$> go !(b $$ var) t ctx'
+    go (VPi str Implicit a b) (RApp t (RSrcPos _ (RVar nm)) Implicit) ctx = do
+      debug "*** \{nm} : \{show a}"
+      let var = VVar (length ctx.env) [<]
+      let ctx' = extend ctx nm a
+      Lam nm <$> go !(b $$ var) t ctx'
     go (VPi str Implicit a b) t ctx = do
       let var = VVar (length ctx.env) [<]
       let ctx' = extend ctx "_" a

src/Lib/Syntax.idr

@@ -131,7 +131,7 @@ Show Raw where
   show (RCase x xs) = foo [ "Case", show x, show xs]
   show (RParseError str) = foo [ "ParseError", "str"]
   show RU = "U"
-  show (RSrcPos pos tm) = show tm
+  show (RSrcPos pos tm) = foo [ "#", show tm]
 
 
 export

src/Lib/Tokenizer.idr

@@ -20,7 +20,7 @@ opChar : Lexer
 opChar = pred isOpChar
 
 identMore : Lexer
-identMore = alphaNum <|> exact "."
+identMore = alphaNum <|> exact "." <|> exact "'"
 
 rawTokens : Tokenizer (Token Kind)
 rawTokens