Skip to content
Snippets Groups Projects
Commit afcea245 authored by Ralf Jung's avatar Ralf Jung Committed by Paolo G. Giarrusso
Browse files

Extend changelog mentioning new `well_founded` module

parent 1e2df25e
No related branches found
No related tags found
1 merge request!327countable.v: prove choose_proper
......@@ -173,7 +173,10 @@ API-breaking change is listed.
- Add lemma `choose_proper` showing that `choose P` respects predicate
equivalence. (by Paolo G. Giarrusso, BedRock Systems)
- Well-founded definitions: Add induction principle `Acc_dep_ind`, a dependent
version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems)
version of `Acc_ind`. This lives in a new module `well_founded` together with
some things that were previously found in `relations`: `Acc_impl`, `wf_guard`,
`wf_guard`, `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`.
(by Paolo G. Giarrusso, BedRock Systems)
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment