Skip to content

List of sub-optimal definitions in Data.List.Base #2359

Open
@JacquesCarette

Description

@JacquesCarette

While looking at PR #2355 from @mildsunrise I noticed a ridiculous number of uses of with. These turn out to not be localized to Data.List.Properties but come from uses of with in Data.List.Base. The vast majority of them can be simplified, with a really nice knock-on effect to simplify quite a few proofs.

But I'm guessing this is yet another case of breaking change, so has to wait until 3.0? I think we should outlaw uses of with in function definitions, if favour of defining explicit 'helper' functions.


Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions