Skip to content

[ fix ] make Data.Nat.Primality.prime⇒nonZero more strict in its explicit. argument#2932

Merged
jamesmckinna merged 1 commit intoagda:masterfrom
jamesmckinna:issue2931
Feb 5, 2026
Merged

[ fix ] make Data.Nat.Primality.prime⇒nonZero more strict in its explicit. argument#2932
jamesmckinna merged 1 commit intoagda:masterfrom
jamesmckinna:issue2931

Conversation

@jamesmckinna
Copy link
Collaborator

@jamesmckinna jamesmckinna commented Feb 5, 2026

Fixes #2931 . No CHANGELOG unless anyone thinks we need one... the upstream issue is the cause.

@jamesmckinna jamesmckinna added this to the v2.4 milestone Feb 5, 2026
@jamesmckinna jamesmckinna added upstream Changes induced by Agda upstream instances labels Feb 5, 2026
@JacquesCarette
Copy link
Collaborator

This is a straight bug-from-the-future bug fix, so I don't think it needs a CHANGELOG either.

@jamesmckinna jamesmckinna added this pull request to the merge queue Feb 5, 2026
Merged via the queue into agda:master with commit fbf6ce1 Feb 5, 2026
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

instances upstream Changes induced by Agda upstream

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Don't be so eager to _, especially in the presence of instances

2 participants