-
list-iter-noinv-specs
this former branch (expr-examples) is kept as a tag because it may have specifications of interest for list.iter such as the `iter_spec_noinv` specs in `examples/proofs/lists_unary`
-
pure_wp/pure_step/no_immediately_pure
This is an alternative definition of `pure_wp` (later just `pure`), that does not use the `may` relation (which reduces to `crash` in case of impurities), but a `pure_step` relation based on `step`, and does not use a predicate `immediately_pure` to rule out impurities. This tag is used to show that this is probably not a good idea, as it seems to be unnecessarily hard, or impossible, to establish contradictions when reaching impurities.
-
pure_wp/pure_step/immediately_pure
This is an alternative definition of `pure_wp` (later just `pure`), that does not use the `may` relation (which reduces to `crash` in case of impurities), but a `pure_step` relation based on `step`, together with an `immediately_pure` predicate in the definition of `pure_wp`. We judged the addition of this predicate to `pure_wp` to be inelegant, but it works fine.
-
simp-based
At this commit and before, pure Hoare-style reasoning is based on simp and so is restricted to confluent computations.
-