Commit 0e228686 authored by Ralf Jung's avatar Ralf Jung
Browse files

add docs and changelog entry

parent 57a3c4ff
......@@ -135,6 +135,10 @@ With this release, we dropped support for Coq 8.9.
threads instead of only a single thread. The derived adequacy lemmas
are unchanged.
**Changes in `heap_lang`:**
* `wp_pures` now turns goals of the form `WP v {{ Φ }}` into `Φ v`.
The following `sed` script helps adjust your code to the renaming (on macOS,
replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
......
......@@ -60,6 +60,8 @@ Tactics to take one or more pure program steps:
well as unary and binary arithmetic operators.
- `wp_pures`: Perform as many pure reduction steps as possible. This
tactic will **not** reduce lambdas/recs that are hidden behind a definition.
If the computation reaches a value, the `WP` will be entirely removed and the
postcondition becomes the new goal.
- `wp_rec`, `wp_lam`: Perform a beta reduction. Unlike `wp_pure`, this will
also reduce lambdas that are hidden behind a definition.
- `wp_let`, `wp_seq`: Reduce a let-binding or a sequential composition.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment