You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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).
The text was updated successfully, but these errors were encountered:
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.
For now I've been simply converting
snake_case
tocamelCase
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).The text was updated successfully, but these errors were encountered: