@@ -939,6 +939,11 @@ rewriteTerm syn = do keyword "rewrite"
939939 return (PRewrite fc using prf sc giving)
940940 <?> "term rewrite expression"
941941
942+-- | Parse a constant and its source span
943+rigCount :: Parsing m => m RigCount
944+rigCount = P.option RigW $ do lchar '1'; return Rig1
945+ <|> do lchar '0'; return Rig0
946+
942947{- |Parses a let binding
943948@
944949Let ::=
@@ -957,18 +962,19 @@ let_ syn = P.try (do keyword "let"
957962 return (buildLets ls sc))
958963 <?> "let binding"
959964 where buildLets [] sc = sc
960− buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc
961− = PLet fc RigW n nfc ty v (buildLets ls sc)
962− buildLets ((fc, pat, ty, v, alts) : ls) sc
965+ buildLets ((fc, rc, PRef nfc _ n, ty, v, []) : ls) sc
966+ = PLet fc rc n nfc ty v (buildLets ls sc)
967+ buildLets ((fc, _, pat, ty, v, alts) : ls) sc
963968 = PCase fc v ((pat, buildLets ls sc) : alts)
964969
965−let_binding syn = do (pat, fc) <- withExtent $ expr' (syn { inPattern = True })
970+let_binding syn = do rc <- rigCount
971+ (pat, fc) <- withExtent $ expr' (syn { inPattern = True })
966972 ty <- P.option Placeholder (do lchar ':'; expr' syn)
967973 lchar '='
968974 v <- expr (syn { withAppAllowed = isVar pat })
969975 ts <- P.option [] (do lchar '|'
970976 P.sepBy1 (do_alt syn) (lchar '|'))
971− return (fc,pat,ty,v,ts)
977+ return (fc,rc,pat,ty,v,ts)
972978 where isVar (PRef _ _ _) = True
973979 isVar _ = False
974980
@@ -1169,7 +1175,7 @@ FunctionSignatureList ::=
11691175@
11701176-}
11711177typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1172−typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount
1178+typeDeclList syn = P.try (P.sepBy1 (do rig <- rigCount
11731179 (x, xfc) <- withExtent fnName
11741180 lchar ':'
11751181 t <- typeExpr (disallowImp syn)
@@ -1180,9 +1186,6 @@ typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount
11801186 t <- typeExpr (disallowImp syn)
11811187 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)
11821188 <?> "type declaration list"
1183− where
1184− rigCount = do lchar '1'; return Rig1
1185− <|> do lchar '0'; return Rig0
11861189
11871190{- | Parses a type declaration list with optional parameters
11881191@