agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

Improve `Data.List.Base` (fix #2359; deprecate use of `with` #2123) #2365

Closed jamesmckinna closed 5 months ago

jamesmckinna commented 5 months ago

Refactor functions taking decidable predicates towards if_then_else_ and away from yes/no:

No attempt to change the proofs in Properties.

jamesmckinna commented 3 months ago

See https://github.com/agda/agda-stdlib/issues/2415#issuecomment-2186511437 for a possible regression introduced by this PR.