Skip to content

get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays

Ralf Jung requested to merge ralf/Z into master

Basically a new take on !677 (closed), but now based on stdpp!439 for Z-based list operations. That said, just changing the existing array lemmas to Z-based indexing would be a massive breaking change, so this keeps the old lemmas around as well.

To express the Z-based lemmas nicely, we need a version of big-star for lists that uses Z-based indexing. So, yet anothert big-op... :( . I ported the most basic lemmas for it, but there are still many big-sep lemmas that need to be ported (and many of these ports are non-trivial).

Fixes stdpp#102.

Merge request reports