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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
