search

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

minor change #105

Closed williamdemeo closed 3 years ago

williamdemeo commented 3 years ago

For the setoid-based development, we can move the definition of ov to a more sensible place, namely, to src/Algebras/Setoid/Basic.lagda.

We cannot do the same for the non-setoid based development because of the way Algebras/Basic.lagda introduces signatures and levels for signatures, so definition of ov in that case will remain in src/Algebras/Products.lagda.

(This PR also includes some other minor mods intended to improve the rendering of the automatically generated html pages.)

williamdemeo commented 3 years ago

Thanks Jacques!

(I'm now fighting with ruby, gems, and jekyll to get gh-pages working again... >_< )

On Sun, Aug 22, 2021 at 3:01 PM Jacques Carette @.***> wrote:

@.**** commented on this pull request.

Good stuff.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/ualib/agda-algebras/pull/105#pullrequestreview-735574900, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA25MJDKHV4XRHX3FDKLLULT6DYLZANCNFSM5CSY6HNA . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .