Tags

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`

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.

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.

At this commit and before, pure Hoare-style reasoning is based on simp and so is restricted to confluent computations.

Osiris with support for OCaml 4.14