Use Integer comparison in Lexer for string length
Nat comparison isn't optimised, so it makes a massive different to
convert to Integer first. This should probably be addressed in the
longer term by having a better way to optimise Nats...
commitf70d4fa4d2abba5a6ab7ee21122280182e20e2ce
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 29 Jul 2018, 17:07 (8 years ago)
parent86126a7
libs/contrib/Text/Lexer/Core.idr+1−1
@@ -82,7 +82,7 @@ getString (MkStrLen str n) = str
8282
8383strIndex : StrLen -> Nat -> Maybe Char
8484strIndex (MkStrLen str len) i
85− = if i >= len then Nothing
85+ = if cast {to = Integer} i >= cast len then Nothing
8686 else Just (assert_total (prim__strIndex str (cast i)))
8787
8888mkStr : String -> StrLen