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.

Sign up for GitHub

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

Jump to bottom

Modular arithmetic based on Data.Nat.Bounded #2257 #2292

Draft
wants to merge 30 commits into
base: master
Choose a base branch
from
Draft

Modular arithmetic based on Data.Nat.Bounded #2257 #2292

wants to merge 30 commits into from

Commits on Jan 25, 2024

  1. sketch of arithmetic mod n, based on Data.Nat.Bounded

    @jamesmckinna
    jamesmckinna committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    1054d17 View commit details
    Browse the repository at this point in the history

  2. RawRing, not only RawSemiring

    @jamesmckinna
    jamesmckinna committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    96d851e View commit details
    Browse the repository at this point in the history

  3. tweaks

    @jamesmckinna
    jamesmckinna committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    edfe817 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2024

  1. streamline the quotient map

    @jamesmckinna
    jamesmckinna committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    5808442 View commit details
    Browse the repository at this point in the history

  2. start of proving the IsRing property

    @jamesmckinna
    jamesmckinna committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    7fbcb46 View commit details
    Browse the repository at this point in the history

Commits on Feb 4, 2024

  1. rename projections

    @jamesmckinna
    jamesmckinna committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    a019dbe View commit details
    Browse the repository at this point in the history

Commits on Feb 5, 2024

  1. more properties

    @jamesmckinna
    jamesmckinna committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    aa7b2bf View commit details
    Browse the repository at this point in the history

  2. progress

    @jamesmckinna
    jamesmckinna committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    9d855cb View commit details
    Browse the repository at this point in the history

Commits on Feb 9, 2024

  1. shim for Data.Nat.Bounded

    @jamesmckinna
    jamesmckinna committed Feb 9, 2024
    Configuration menu
    Copy the full SHA
    0c9eed6 View commit details
    Browse the repository at this point in the history

  2. local change to Bounded shim

    @jamesmckinna
    jamesmckinna committed Feb 9, 2024
    Configuration menu
    Copy the full SHA
    d5bed3a View commit details
    Browse the repository at this point in the history

  3. incremental progress

    @jamesmckinna
    jamesmckinna committed Feb 9, 2024
    Configuration menu
    Copy the full SHA
    0f9ec78 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2024

  1. revised to reflect improvements to ℕ<

    @jamesmckinna
    jamesmckinna committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    532e3ed View commit details
    Browse the repository at this point in the history

  2. remove shim dependency

    @jamesmckinna
    jamesmckinna committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    e3bf662 View commit details
    Browse the repository at this point in the history

  3. remove shim dependency

    @jamesmckinna
    jamesmckinna committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    b299856 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2024

  1. further revised to reflect improvements to ℕ<

    @jamesmckinna
    jamesmckinna committed Feb 11, 2024
    Configuration menu
    Copy the full SHA
    8caf9ac View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2024

  1. committed Data.Nat.Bounded.* against subsequent PR

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    d7447d0 View commit details
    Browse the repository at this point in the history

  2. tweak syntax to distinguish from Data.Integer.Modulo

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    508249f View commit details
    Browse the repository at this point in the history

  3. tweaks

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    cccf3a8 View commit details
    Browse the repository at this point in the history

  4. refactoring Data.Integer.Modulo.Properties via revised `Data.Nat.Bo… 

    …unded.Properties`
    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    b51bc24 View commit details
    Browse the repository at this point in the history

  5. nonZeroModulus

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    e235c9a View commit details
    Browse the repository at this point in the history

  6. using nonZeroModulus

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    4e9921a View commit details
    Browse the repository at this point in the history

  7. refactoring

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    fbcec66 View commit details
    Browse the repository at this point in the history

  8. refactoring lemmas

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    6d7e7ac View commit details
    Browse the repository at this point in the history

  9. arithmetic mod n lemmas

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    e3d3243 View commit details
    Browse the repository at this point in the history

  10. additional arithmetic

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    692e847 View commit details
    Browse the repository at this point in the history

  11. integers mod n form a Ring

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    0f6f0ce View commit details
    Browse the repository at this point in the history

  12. moved Modulo to Modulo.Base

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    8cf05cb View commit details
    Browse the repository at this point in the history

  13. knock-on from moving Modulo to Modulo.Base; CHANGELOG

    @jamesmckinna
    jamesmckinna committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    b78f407 View commit details
    Browse the repository at this point in the history

  14. Merge branch 'master' into modular-arithmetic

    @jamesmckinna
    jamesmckinna authored Feb 12, 2024
    Configuration menu
    Copy the full SHA
    aa22e03 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2024

  1. 'rebasing' against revised /updated agda#2257

    @jamesmckinna
    jamesmckinna committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    4ab04f1 View commit details
    Browse the repository at this point in the history