Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add a few algebraic structures missing from the Algebra.Construct.Pointwise #2555

Merged
merged 5 commits into from
Jan 19, 2025

Conversation

bsaul
Copy link
Contributor

@bsaul bsaul commented Jan 16, 2025

This PR adds a few structures/bundles currently missing from Algebra.Construct.Pointwise, namely:

  • isNearSemiring
  • isSemiringWithoutOne
  • isCommutativeSemiringWithoutOne
  • isCommutativeSemiring
  • isIdempotentSemiring
  • isKleeneAlgebra
  • isQuasiring
  • isCommutativeRing

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Jan 16, 2025

Bradley, thanks for mopping up the missing pieces of #2381 ! A nice first PR.

NB we'll need a CHANGELOG entry, and while we should #2557 begin again for v2.3 with a clean CHANGELOG rather than the v2.2 one currently in-place on master, the fact that this PR touches only one module should mean that your commits won't give rise to merge conflicts... so suggest you add those entries now?

@bsaul
Copy link
Contributor Author

bsaul commented Jan 16, 2025

Bradley, thanks for mopping up the missing pieces of #2381 ! A nice first PR.

Thanks!

NB we'll need a CHANGELOG entry, and while we should #2557 begin again for v2.3 with a clean CHANGELOG rather than the v2.2 one currently in-place on master, the fact that this PR touches only one module should mean that your commits won't give rise to merge conflicts... so suggest you add those entries now?

To be clear, you'd like me to add something like the following?

Version 2.3-dev
===========

Additions to existing modules
-----------------------------

* In `Algebra.Construct.Pointwise`:
  ```agda
  isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
             IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
  
  nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)

  ...etc...

@jamesmckinna
Copy link
Contributor

... Yup! It's boring but exactly what's required.

@bsaul
Copy link
Contributor Author

bsaul commented Jan 16, 2025

... Yup! It's boring but exactly what's required.

Cool. Added.

@jamesmckinna jamesmckinna added this to the v2.3 milestone Jan 16, 2025
CHANGELOG.md Outdated Show resolved Hide resolved
Copy link
Contributor

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This all looks good now!
Just needs a second approval.

@jamesmckinna jamesmckinna added this pull request to the merge queue Jan 19, 2025
Merged via the queue into agda:master with commit 908e015 Jan 19, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants