(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definition: JNRJQSM                                                        *)
(* Chapter: Packing                                                           *)
(* Author: Thomas C. Hales                                                    *)
(* Date: Feb 14, 2010                                                         *)
(* ========================================================================== *)


(* This is the truncation to initial segments.  
    NB. There is a shift in the index by 1, because we are viewing a list of length d+1 as a d-simplex.
   d_j in the flypaper.
*)


module type Jnrjqsm_def_type = sig
  val JNRJQSM : thm
end;;

flyspeck_needs "general/sphere.hl";;

module Jnrjqsm : Jnrjqsm_def_type = struct

(*
  let TRUNCATE_SIMPLEX = new_definition
    `truncate_simplex j (ul:(A) list) = 
      @vl. ( LENGTH vl = j+1 /\ initial_sublist vl ul)`;;
*)

  let JNRJQSM = Sphere.TRUNCATE_SIMPLEX;;

end;;