• Zhen Zhang's avatar
    Simplify and update · 3fd612a9
    Zhen Zhang authored
    - evmap is dropped
    - per-item invariant is implemented with inv-in-inv
    - peritem.v is simplified by proving an ad-hoc iter spec
    - update to latest iris
    - related fixes
    3fd612a9
flat.v 12.6 KB