Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
gares authored Dec 2, 2024
1 parent 9f73e90 commit d55a78c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion apps/derive/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ Currently there are 3 groups:
+ `map` map over a container
+ `param1_functor` functoriality lemmas (map over the param1 translation)
+ `lens` and `lens_laws` generate lenses focusing on record fields and some
equations governing setter/setters
equations governing setter/setters (aka record update syntax)
- `derive.legacy` contains derivations superseded by `std`:
+ `eq` and `eqOK` generate sound equality tests in quadratic time/space, see
[Deriving proved equality tests in Coq-elpi](http://drops.dagstuhl.de/opus/volltexte/2019/11084/)
Expand Down

0 comments on commit d55a78c

Please sign in to comment.