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

Proof names #11

Open
clayrat opened this issue Aug 21, 2017 · 1 comment
Open

Proof names #11

clayrat opened this issue Aug 21, 2017 · 1 comment

Comments

@clayrat
Copy link
Collaborator

clayrat commented Aug 21, 2017

For now I've been simply converting snake_case to camelCase in proof names, but I think once Bip proofs are done, we should go through them and rename to reflect the names of actual Bip functions (e.g., subMask* -> bimMinus* etc).

@sbp
Copy link
Owner

sbp commented Aug 23, 2017

Agreed, and I was thinking about renaming some of the functions anyway. My plan was to go through the Idris libraries looking at existing arithmetic functions to see how they're named, and then to copy that style as much as possible in this library. Since this is Idris, it'd be better to be consistent with Idris rather than with Coq. In any case the existing naming is not very consistent—e.g. I'm using things like "DMO" to abbreviate "doubleMinusOne", whereas there's also "pred" for predecessor to express minus one in other cases.

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

No branches or pull requests

2 participants