File: TODO.org

package info (click to toggle)
coq-deriving 0.2.2-1
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 256 kB
  • sloc: ml: 28; makefile: 22
file content (8 lines) | stat: -rw-r--r-- 434 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
 
* Documentation
* Clean up code
* Ensure equality and order operations are simplified properly
* Check why it is not possible to derive the mixin directly in the instance
E.g. this does not work:
HB.instance Definition _ := [derive eqMixin for foo].
* Find a better way of writing packing functions (cf. infer.v and the derive notation in eqtype.v)
* By default, [derive nored eqMixin for ...] does not simplify the type of the mixin