Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some modular arithmetic #550

Merged
merged 20 commits into from
Nov 1, 2021
Merged

Some modular arithmetic #550

merged 20 commits into from
Nov 1, 2021

Conversation

aljungstrom
Copy link
Contributor

@aljungstrom aljungstrom commented Apr 29, 2021

This PR contains some basic modular arithmetic (defined on Fin). I did this ages ago and haven't thought much about it since, but it seems to work pretty well.

I also threw in a definition of Z/nZ in Group.Instances.

@ecavallo ecavallo marked this pull request as draft May 21, 2021 13:16
@aljungstrom aljungstrom marked this pull request as ready for review October 28, 2021 18:00
@aljungstrom
Copy link
Contributor Author

@ecavallo Ok, finally got to it... Se what you think

@ecavallo
Copy link
Collaborator

A lot of the results in Data.Fin.Arithmetic are about more than Fin. What do you think about moving these to some file under Data.Nat?

@aljungstrom
Copy link
Contributor Author

A lot of the results in Data.Fin.Arithmetic are about more than Fin. What do you think about moving these to some file under Data.Nat?

Very true:-) better now?

@ecavallo
Copy link
Collaborator

Thanks. One last thing, since modIndBase and modIndStep are no longer private, could you fill in their type signatures?

@aljungstrom
Copy link
Contributor Author

Wups.. fixed

@ecavallo ecavallo merged commit a1d2bb3 into agda:master Nov 1, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants