ualib / agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)
https://ualib.github.io/agda-algebras/
Creative Commons Attribution Share Alike 4.0 International
29 stars 7 forks source link

major refactoring #241

Open williamdemeo opened 10 months ago

williamdemeo commented 10 months ago
williamdemeo commented 10 months ago

@JacquesCarette Thank you for continuing to care about this project and commenting on PRs. I really appreciate your input! 🤗

A couple of issues with this PR (recorded here for my own reference), to be addressed before merging:

  1. Refactor proofs marked "TODO".
  2. Incorporate the above suggested minor changes (which simply remove commented-out code).
  3. Remove notation changes (α -> a, β -> b, etc.) from this PR and make a new one solely for notation changes.
  4. Make a new permanent branch off of the latest master; call it something like "Agda 2.6.3/1.7.2".
  5. Make a new "official release" of agda-algebras based off latest master, in case anyone wants to use the library with Agda 2.6.3 and Agda Standard Library 1.7.2.