eberlm at in.tum.de
Mon Jun 18 14:23:52 CEST 2018
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.
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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev