cleaned up some code; made proofs clearer (to me)

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

28 stars 7 forks source link

cleaned up some code; made proofs clearer (to me) #220

Closed williamdemeo closed 2 years ago

williamdemeo commented 2 years ago

Still have to make sure text describes code in the latter sections. (I'm quite sure there are still sentences referring to the entailment type.) I'll get to that after dinner.

JacquesCarette commented 2 years ago

Also: if there are length issues, let me know asap. I'm going at buying a few lines. And getting a few lines early in the paper tends to have a knock-on effect of freeing more lines later on, because of the way TeX's algorithms work.