search

affeldt-aist / coq-robot

Mathematics of Rigid Body Transformationss using Coq and MathComp
26 stars 2 forks source link

move nsatz to MathComp -Analysis? #33

Open affeldt-aist opened 3 years ago

affeldt-aist commented 3 years ago

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 too? Or in MathComp? @CohenCyril @thery

thery commented 3 years ago

in math-comp/analysis#383 we could use the new ring of Kazuhiko but I didn't want to add a new depency. For coq-robot, we actually use the grobner basis computation but maybe with some work this could be also a simpl ring I need to investigate.