Laurent Théry (Apr 28 2021 at 11:18): Laurent Théry (Apr 28 2021 at 11:18):I was wondering if someone knows any attemt to have quaternions with the mathcomp library?
Reynald Affeldt (Apr 28 2021 at 11:26):you mean something like that: https://github.com/affeldt-aist/coq-robot/blob/master/quaternion.v ?
Laurent Théry (Apr 28 2021 at 11:38):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?
Reynald Affeldt (Apr 28 2021 at 11:48):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