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 the Setoidal structure of a (free) Monoid on List #2360

Closed
jamesmckinna opened this issue Apr 12, 2024 · 1 comment · Fixed by #2393
Closed

Add the Setoidal structure of a (free) Monoid on List #2360

jamesmckinna opened this issue Apr 12, 2024 · 1 comment · Fixed by #2393

Comments

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Apr 12, 2024

(Extracted from #2350)
Module Data.List.Relation.Binary.Equality defines the Setoid lifting of equality from a Setoid on A to one on List A.

But nowhere that I can find is the ++-[]-monoid bundle/structure etc. defined for this Setoid... so we should add it.

See this blob #2393 for one possible implementation.

Issues:

  • where should this construction live?
  • what else should be added along these lines?
  • what other 'obvious' Setoid liftings are missing?

NB this comment seems never to have been acted upon cf. #568

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented May 22, 2024

Downstream breaking (?) refactoring(s) (v3.0 or hypothetical-rewrite?)

  • Data.List.Properties.Setoid
  • Data.List.Properties.Propositional
    ???

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant