Skip to content

Data.List.Base.all: fix warning#2992

Merged
MatthewDaggitt merged 4 commits into
agda:masterfrom
Brian-ED:list-base-all-warning
May 6, 2026
Merged

Data.List.Base.all: fix warning#2992
MatthewDaggitt merged 4 commits into
agda:masterfrom
Brian-ED:list-base-all-warning

Conversation

@Brian-ED

@Brian-ED Brian-ED commented May 2, 2026

Copy link
Copy Markdown
Contributor

Fix warning for Data.List.Base.all which refered to Nat instead of Bool, issue #2991

@Brian-ED

Brian-ED commented May 2, 2026

Copy link
Copy Markdown
Contributor Author

I noticed a typo in the changelog, will fix

@Taneb Taneb linked an issue May 5, 2026 that may be closed by this pull request
@MatthewDaggitt MatthewDaggitt added this to the v2.4 milestone May 6, 2026
@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue May 6, 2026
Merged via the queue into agda:master with commit 0441b4c May 6, 2026
12 checks passed
@Brian-ED Brian-ED deleted the list-base-all-warning branch May 6, 2026 16:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Data.List.Base.all incorrect warning

4 participants