legacy/oldpacking/JNRJQSM_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: JNRJQSM                                                        *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 14, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10
  11 (* This is the truncation to initial segments.
  12     NB. There is a shift in the index by 1, because we are viewing a list of length d+1 as a d-simplex.
  13    d_j in the flypaper.
  14 *)
  15
  16
  17 module type Jnrjqsm_def_type = sig
  18   val JNRJQSM : thm
  19 end;;
  20
  21 flyspeck_needs "general/sphere.hl";;
  22
  23 module Jnrjqsm : Jnrjqsm_def_type = struct
  24
  25 (*
  26   let TRUNCATE_SIMPLEX = new_definition
  27     `truncate_simplex j (ul:(A) list) =
  28       @vl. ( LENGTH vl = j+1 /\ initial_sublist vl ul)`;;
  29 *)
  30
  31   let JNRJQSM = Sphere.TRUNCATE_SIMPLEX;;
  32
  33 end;;