@@ -25,6 +25,9 @@ negative = Refl
2525negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""
2626negativeEnd = Refl
2727
28+negativeLength : prim__strSubstr 4 (-4) firstSentence = ""
29+negativeLength = Refl
30+
2831main : IO ()
2932main = do putStrLn $ prim__strSubstr 1 1004 foo
3033 printLn $ length $ prim__strSubstr 1 1000 foo
@@ -40,6 +43,8 @@ main = do putStrLn $ prim__strSubstr 1 1004 foo
4043 putStrLn $ show (length (prim__strSubstr 3 8000 input))
4144 putStrLn $ prim__strSubstr (-13) 18 input
4245 putStrLn $ show (length (prim__strSubstr (-13) 18 input))
46+ putStrLn $ prim__strSubstr 4 (-4) input
47+ putStrLn $ show (length (prim__strSubstr 4 (-4) input))
4348 -- Single-byte dynamic string
4449 input <- getLine
4550 putStrLn $ prim__strSubstr 3 8 input
@@ -48,4 +53,6 @@ main = do putStrLn $ prim__strSubstr 1 1004 foo
4853 putStrLn $ show (length (prim__strSubstr 3 8000 input))
4954 putStrLn $ prim__strSubstr (-13) 18 input
5055 putStrLn $ show (length (prim__strSubstr (-13) 18 input))
56+ putStrLn $ prim__strSubstr 4 (-4) input
57+ putStrLn $ show (length (prim__strSubstr 4 (-4) input))
5158