Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-19 12:37:18 -0800 (Mon, 19 Dec 2005)
Revision: 8321
Log message:

      Here is a slightly different approach, where the idea
      is to rewrite
      
         substl{substl{'e; 'l1}; 'l2}
         <-->
         substl{'e; append{'l1; 'l2}}
      
      To do so, we need to know that 'l1 and 'l2 are lists.
      The Itt_hoas_vector.bindn_to_list_of_fun is such
      an attempt:
      
         bind{'n; x. 'e['x]}
         <-->
         bind{'n; x. 'e[list_of_fun{i. nth_elem{'x; 'i}; 'n}]}
      
      Unfinished, the proof is not easy AFAIK.
      

Changes  Path
+5 -0 metaprl/theories/itt/extensions/base/itt_list3.ml
+1079 -1027 metaprl/theories/itt/extensions/base/itt_list3.prla
+1 -0 metaprl/theories/itt/reflection/core/OMakefile
+15 -0 metaprl/theories/itt/reflection/core/itt_hoas_vector.ml
+2057 -960 metaprl/theories/itt/reflection/core/itt_hoas_vector.prla
+7 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml