git.iko.soy/Idris-dev
on master help sign in
Use Integer comparison in Lexer for string length
f70d4faEdwin Brady
libs/contrib/Text/Lexer/Core.idr+1−1
compare with master
unifiedsplit
@@ -82,7 +82,7 @@ getString (MkStrLen str n) = str
82
82
83strIndex : StrLen -> Nat -> Maybe Char
83strIndex : StrLen -> Nat -> Maybe Char
84strIndex (MkStrLen str len) i
84strIndex (MkStrLen str len) i
85− = if i >= len then Nothing
85+ = if cast {to = Integer} i >= cast len then Nothing
86 else Just (assert_total (prim__strIndex str (cast i)))
86 else Just (assert_total (prim__strIndex str (cast i)))
87
87
88mkStr : String -> StrLen
88mkStr : String -> StrLen