Stream: math-comp users

Topic: quaternions


view this post on Zulip Laurent Théry (Apr 28 2021 at 11:18):

I was wondering if someone knows any attemt to have quaternions with the mathcomp library?

view this post on Zulip Reynald Affeldt (Apr 28 2021 at 11:26):

you mean something like that: https://github.com/affeldt-aist/coq-robot/blob/master/quaternion.v ?

view this post on Zulip 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?

view this post on Zulip 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