[isabelle-dev] quaternions

[Manuel Eberl]

I would also have suggested an AFP entry.

> let reflect_along = new_definition
>  `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;
Think of it as x being the direction of a ray of light hitting a mirror
(in the shape of a hyperplane through the origin with normal vector a)
and being reflected. The result is the direction of the reflected ray.

Where it belongs I cannot say; that depends on what kinds of results are
proven about it. I for one would consider this a very ‘applied’ concept
(I know it from ray tracing), so unless we have a concrete application
for it, I'm not sure we need it at all.

Manuel


On 2018-06-18 14:17, Lars Hupel wrote:
>> So where does this material belong? Arguably not in Analysis, which is already too large.
> Why not a regular AFP entry?
>
> Cheers
> Lars
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180618/cfb02d7b/attachment-0002.html>