Skip to content

add some number instances for Assoc, Comm, ...

Ralf Jung requested to merge ralf/numbers into master

Inspired by https://github.com/bedrocksystems/BRiCk/blob/614b303aa6370ecfcb354ec9715e65a5a5a28630/theories/prelude/numbers.v, but I didn't add all of their instances, there's so many of them... so I went for the key properties (assoc, comm, neutral and absorbing elements) of the core operations (add, sub, mul, div).

Edited by Ralf Jung

Merge request reports

Loading