I was wondering if someone knows any attemt to have
quaternions with the
you mean something like that: https://github.com/affeldt-aist/coq-robot/blob/master/quaternion.v ?
Perfect this is exactly what I was searching. Would it make sense to have a version without the rotation things that could be compiled with the currrent mathcomp? Did you also try the octonions?
I guess you are talking about extracting the part that depends only on mathcomp into a separate development (or into mathcomp). I think that this would make sense. (Of course, I’d like to keep the rotation part compiling but that can stay into coq-robot.) I haven’t tried octonions.
Last updated: Feb 08 2023 at 07:02 UTC