Skip to content
Snippets Groups Projects
Commit f05baf13 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

CHANGELOG.

parent 7ab0cff7
No related branches found
No related tags found
1 merge request!125Lookup total lemmas
...@@ -30,6 +30,10 @@ API-breaking change is listed. ...@@ -30,6 +30,10 @@ API-breaking change is listed.
- Add tactic `set_unfold in H`. - Add tactic `set_unfold in H`.
- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`, - Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`,
`TCEq`, and `TCDiag`. `TCEq`, and `TCDiag`.
- Add type class `LookupTotal` with total lookup operation `(!!!) : M → K → A`.
Provide instances for `list`, `fin_map`, and `vec`, as well as corresponding
lemmas for the operations on these types. The instance for `vec` replaces the
ad-hoc `!!!` definition.
## std++ 1.2.1 (released 2019-08-29) ## std++ 1.2.1 (released 2019-08-29)
......
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