4 ms·

Dex proves indexing correctness without a full dependent type system, including loops. See: https://github.com/google-research/dex-lang/pull/969 https://github

by amkkma 4y ago

Dex proves indexing correctness without a full dependent type system, including loops. See: https://github.com/google-research/dex-lang/pull/969 https://github.com/google-research/dex-lang/pull/969 and https://github.com/google-research/dex-lang/blob/5cbbdc50ce0d2798f25cd8e2370b7a091b413717/examples/levenshtein-distance.dx https://github.com/google-research/dex-lang/blob/5cbbdc50ce0... for examples

ChrisRackauckas 4y ago
Yes, but that doesn't handle this case. I discussed a case of indexing in the bounds which is still incorrect.