Skip to content

max is a monoid operator #2093

Description

@affeldt-aist

In PR #2060, it was question
of introducing another instance of Monoid.Law.sort on Order.max, which
causes a problem.

We should have a "max is a monoid operator" structure (likely Order.BPreorder or something like that)
and put the monoid instance on it (and then ensure that both ereal and
nonneg have the BPreorder instance).

Reference: #2060 (comment)

fyi: @holgerthies @yosakaon @proux01

Metadata

Metadata

Assignees

No one assigned

    Labels

    experiment 🧪This issue/PR is very experimental

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions