coq-robot

coq-robot copied to clipboard

reintroduce a type for angle (wip)

8

affeldt-aist

move nsatz to MathComp -Analysis?

1

There is an instance of nsatz with rcfType in https://github.com/affeldt-aist/coq-robot/blob/master/ssr_ext.v Similarly, there is an instance of nsatz with realType in https://github.com/math-comp/analysis/pull/383 Should the rcfType instance of nsatz move in Analysis...

affeldt-aist

https://github.com/affeldt-aist/coq-robot/blob/ce7c75a7a2a990c446735299ad9ca04e8f621ebd/ssr_ext.v#L116-L121 this requires to first declare a numDomainType structure for matrices

affeldt-aist

fyi: @thery

affeldt-aist