Skip to content

ITP camera-ready
Compare
Choose a tag to compare
@tlringer tlringer released this 20 Jun 23:31
· 835 commits to master since this release
itp+equiv
de9de1d

This release builds on the ITP submission release with a few new features:

  • An option Set DEVOID search prove coherence to tell Find ornament to generate a proof of coherence
  • An option Set DEVOID search prove equivalence to tell Find ornament to generate proofs of section and retraction
  • Documentation and tests for these options
  • An updated case study that:
    • Uses DEVOID's generated functions (the old case study was not doing this by mistake)
    • Uses DEVOID's generated equivalences
    • Uses a trick from a reviewer to produce more meaningful numbers that do not include printing time
  • A few bug fixes:
    • SECTION/RETRACTION recurse into the algorithm as well
    • Lazy eta expansion is slightly smarter
    • Packing to deal with non-primitive projections is much smarter
  • Extra documentation in existing examples, especially for user-friendly types
  • Documentation for restrictions on inputs
  • Lengthy, expanded README
Assets 2
Loading