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

chop: %Int => modInt #105

Closed
wants to merge 1 commit into from
Closed

chop: %Int => modInt #105

wants to merge 1 commit into from

Conversation

daejunpark
Copy link
Contributor

Do not merge. Just to see what happens.

@kframework-bot
Copy link

Can one of the admins verify this patch?

@pirapira
Copy link
Contributor

pirapira commented Jan 2, 2018

Oh, sorry, I rebased a branch that's not mine.

@dwightguth
Copy link
Member

Do we want to merge this?

@daejunpark
Copy link
Contributor Author

daejunpark commented Jan 8, 2018

@dwightguth Not sure. Clearly, %Int is wrong when I is negative, although @ehildenb believes that no negative values can appear during the execution. Still this change makes sense and better to be merged just in case. But the thing is that there are many other places where such a questionable %Int is still used instead of modInt, and I'm not sure how much merging this single change will make the definition robust.

I'd like to ask someone to carefully go over the definition and fix them all at once.

@daejunpark daejunpark mentioned this pull request Jan 11, 2018
@daejunpark
Copy link
Contributor Author

close this and open #115

@daejunpark daejunpark closed this Jan 11, 2018
@daejunpark daejunpark deleted the fix-mod-int branch March 12, 2018 06:26
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

4 participants