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

Add a number notation for ring #841

Merged
merged 5 commits into from Mar 4, 2022
Merged

Add a number notation for ring #841

merged 5 commits into from Mar 4, 2022

Commits on Mar 3, 2022

  1. [CI] Update Nix CI

    @proux01
    proux01 committed Mar 3, 2022
    Configuration menu
    Copy the full SHA
    cdcfada View commit details
    Browse the repository at this point in the history

  2. Add a number notation in AC_scope

    @proux01
    proux01 committed Mar 3, 2022
    Configuration menu
    Copy the full SHA
    8b34f31 View commit details
    Browse the repository at this point in the history

  3. Add %N for natural numbers 

    This is done in preparation to the addition of a number notation in
scope ring_scope. So we want to avoid natural number constants such as
2 or 3 to be interpreted in ring_scope.
    @proux01
    proux01 committed Mar 3, 2022
    Configuration menu
    Copy the full SHA
    15012fb View commit details
    Browse the repository at this point in the history

  4. Add a number notation for ring 

    Now, 12 or 42 are read as 12%:R or 42%:R in scope ring_scope.
If ssrint is imported, -6 is read as (-6)%:~R.

One may have to add a few %N in code that was using concrete
nat values in scope ring_scope.
    @proux01
    proux01 committed Mar 3, 2022
    Configuration menu
    Copy the full SHA
    3bee1da View commit details
    Browse the repository at this point in the history

  5. Remove useless %:R on numbers 

    2 is now a notation for 2%:R
    @proux01
    proux01 committed Mar 3, 2022
    Configuration menu
    Copy the full SHA
    dd6532a View commit details
    Browse the repository at this point in the history