Skip to content

[ refactor ] make step a manifest field of Data.Nat.PseudoRandom.LCG.Generator#2937

Merged
jamesmckinna merged 2 commits intoagda:masterfrom
jamesmckinna:manifest-LCG-step
Feb 9, 2026
Merged

[ refactor ] make step a manifest field of Data.Nat.PseudoRandom.LCG.Generator#2937
jamesmckinna merged 2 commits intoagda:masterfrom
jamesmckinna:manifest-LCG-step

Conversation

@jamesmckinna
Copy link
Copy Markdown
Collaborator

Fixes #2936 plus some cosmetic tidying up of the import dependencies.

@jamesmckinna jamesmckinna changed the title [ refactor ] make step a manifest field of Data.Nat.LCG.Generator [ refactor ] make step a manifest field of Data.Nat.PseudoRandom.LCG.Generator Feb 8, 2026
@jamesmckinna jamesmckinna requested a review from Taneb February 9, 2026 10:06
@jamesmckinna jamesmckinna added this pull request to the merge queue Feb 9, 2026
Merged via the queue into agda:master with commit 76e7589 Feb 9, 2026
12 checks passed
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.

[ discussion ] module-level definitions vs. manifest fields in records

3 participants