4 ms·

There are tools to do exactly that (I don't remember the name of what we used at university, alas). And no, I do not want to run a SMT solver against anything b

• catnaroek 11y ago
  Most index manipulation is fairly simple. For instance, if the result of `str.find(pat)` is `Some(pos)`, then you know that: (0) `pos <= str.len()`. (1) `pos` is actually the beginning of a character - it makes sense to split the string at the position `pos`. These things are easy to check - there is not even any multiplication involved! - but a conventional type checker won't do. Much of the pain of using dependent types is the result of sticking to unification as the only basis for type-checking.
  • llogiq 11y ago
    On the contrary, it's actually rather easy to use the type checker to encode this: Just make a wrapper type CharIdx(usize) that encodes the fact that the enclosed value is a valid char position and implement Index for it using unchecked indexing. Also implement Index for usize with the usual check for bounds and valid character position.