projects_discrete_geom/fejestoth12/defs.hl

   1 (* for 2D hexagon perimeter theorem *)
   2
   3 let ell_uvx = new_definition `ell_uvx (x1:real) (x2:real) (x3:real)
   4   (x4:real) (x5:real) (x6:real) =
   5   (let et2 = eta_x x1 x2 x3 pow 2 in
   6      sqrt(et2 - (x1/ &4)) + sqrt(et2 - (x2/ &4)))`;;
   7
   8 let ell_vx2 = new_definition `ell_vx2 (x1:real) (x2:real) (x3:real)
   9   (x4:real) (x5:real) (x6:real) =
  10   (let et2 = eta_x x1 x2 x3 pow 2 in
  11      sqrt(et2 - (x2/ &4)))`;;