Skip to content

Rename Data.List.Properties.*-is-foldr  #2516

Open
@jamesmckinna

Description

@jamesmckinna

I wouldn't call this partition-is-foldr but partition-as-foldr , or partition-via-foldr. And yes, foldr being the List eliminator, we need to be careful to not have an explosion of these. Having said that, I'm fine with partition as it is an important function.

But we already have

  • id-is-foldr
  • ++-is-foldr
  • map-is-foldr
  • ...

So it does explode into a deprecation-fest if we follow your lead? v3.0?

Originally posted by @jamesmckinna in #2505 (comment)

Proposal: all *-is-fold* lemmas be renamed, and the old names deprecated.

Issue: what alternative naming policy?

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions