Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
Shouldn't we change the milestone to 2.x? Then can we get this consistency for 1.x by backporting the changes from 2.x?
Now I think `%/` in `int_scope` should be redefined to let its arguments inherit `int_scope`, i.e., ```coq Notation "m %/ d" := (divz m%Z d%Z) : int_scope. ``` BTW, the...
I'm also a bit surprised since `m` and `d` in `(m %/ d)%Z` do not seem to use `int_scope` to interpret notations. I'm taking a look at the reference manual...
> I guess the difference is between deep scope opening (with `m%Z` the entire term `m` gets interpreted in scope `int_scope`) versus shallow (in the second case, only the topmost...
Thanks. That explains the issue! What we need is probably: ```coq Arguments divz (m d)%int_scope%ring_scope ``` where my intention is to give priority to `int_scope` (placing `int_scope` on top of...
Also, always opening `ring_scope` when opening `int_scope` in this order is probably what I mean by `int_scope` is a *subscope* of `ring_scope`.
@affeldt-aist I don't understand why you think lemmas about `finType` subsumes lemmas about `eqType`.
I added pointers to issues dedicated to some items.
> Is it also possible to solve matrix equations by erasing the size information, e.g., embedding matrices to infinitely large matrices represented as finmap? A potential answer: https://doi.org/10.2168/LMCS-8(2:13)2012 (see Section...
One can bridge finsets and machine integers to have fast membership lookup in extracted code: https://hal.inria.fr/hal-01251943v1 https://github.com/artart78/coq-bitset https://github.com/ejgallego/ssrbit