Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib
Rename _plus
/_minus
into _add
/_sub
to be consistent with Coq's current convention for numbers.
Following the discussion at iris!821 (merged)
Edited by Robbert Krebbers
Merge request reports
Activity
Please register or sign in to reply