Merge remote-tracking branch 'origin/master' into v0.9.7.0-alpha1

FStarLang · Jun 26, 2019 · df5d281 · df5d281
2 parents 0ffeb7f + 11698f1
commit df5d281
Show file tree

Hide file tree

Showing 637 changed files with 16,077 additions and 16,778 deletions.
diff --git a/doc/tutorial/code/exercises/Ex01a.fst.hints b/doc/tutorial/code/exercises/Ex01a.fst.hints
@@ -18,7 +18,7 @@
         "projection_inverse_FStar.Pervasives.V_v"
       ],
       0,
-      "99595fc8ed70e62a330c52abcad03c48"
+      "502378d8a0efd4b00759039b7fc7d098"
     ],
     [
       "Ex01a.checkedRead",
@@ -27,7 +27,7 @@
       1,
       [ "@query", "projection_inverse_BoxBool_proj_0" ],
       0,
-      "1e6572f013abd0e4d23713936ce3532d"
+      "956cd4214cd85d8531d07be52e62a65b"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex03a.fst.hints b/doc/tutorial/code/exercises/Ex03a.fst.hints
@@ -17,7 +17,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "084e7b5e66a3d01a60b5d2ee4f61cb4c"
+      "37459c99e86c2841af26bc9cdfcf3f5e"
     ],
     [
       "Ex03a.factorial",
@@ -35,7 +35,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "761fa1ed9ab18365ac34334c281a608a"
+      "01928761149bff193f74a789603bb5ff"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex03b.fst.hints b/doc/tutorial/code/exercises/Ex03b.fst.hints
@@ -16,7 +16,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "e5a19431223106290f87dcb7f89e8d7e"
+      "49da0b1da3644e0194f5d308e30f461d"
     ],
     [
       "Ex03b.fibonacci",
@@ -33,7 +33,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "64f40377ca53c49b8f7514884f73ab1e"
+      "6c3e5132af9812fc3d08d03c6ed1fd92"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex03c.fst.hints b/doc/tutorial/code/exercises/Ex03c.fst.hints
@@ -16,7 +16,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "8242c45998111c0f3cf7058ffe4cccbb"
+      "123a5e436db39338f645b3dd9050fe33"
     ],
     [
       "Ex03c.fibonacci",
@@ -33,7 +33,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "83566e9f7942fdb1f2b6019f01983f8b"
+      "25d0e0e7ea0cf71d67b858159f13d7df"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex04a.fst.hints b/doc/tutorial/code/exercises/Ex04a.fst.hints
@@ -16,7 +16,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "db45d1d3344908c32a60d7d0f4fc4ef5"
+      "a7ec820f4990c7faf7eb5c6880a39904"
     ],
     [
       "Ex04a.append",
@@ -30,7 +30,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "3a2f109e9eb69bca8bed2e5450bc40a5"
+      "ca81cd8eb0404265637a92ae56ccd796"
     ],
     [
       "Ex04a.length",
@@ -47,7 +47,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "b4a5febe5274387fe368302d5d8c7c43"
+      "415ca769c873205d2443044d164d4274"
     ],
     [
       "Ex04a.append",
@@ -61,7 +61,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "bce943150c47fe14956589e0811274ef"
+      "c303f91544ddcb0b8b1eab366395f3e7"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex04b.fst.hints b/doc/tutorial/code/exercises/Ex04b.fst.hints
@@ -16,7 +16,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "5306011e04567b0471f6a4e6aa40249e"
+      "5daf9992e7d56f72c3b775088b6bbabb"
     ],
     [
       "Ex04b.append",
@@ -31,7 +31,7 @@
         "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "2fe8110ce7f47dc3047e63cba165e23b"
+      "7cc4dbc65f59fbc15fff5ea0886832d0"
     ],
     [
       "Ex04b.length",
@@ -48,7 +48,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "8dc72940e5e178118149712468f41839"
+      "ac5e7d22eeab5b3a24b7f2d95b74f4d2"
     ],
     [
       "Ex04b.append",
@@ -62,7 +62,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "a4f7f810ad4382b1c4e5855b9c906b5b"
+      "e3a730e8f8603d19b14a9e6d0945b628"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex04c.fst.hints b/doc/tutorial/code/exercises/Ex04c.fst.hints
@@ -13,7 +13,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "54fb894d99e4828c13e8f666d07d821d"
+      "0b69b16bcfa64af646fc863c134401ad"
     ],
     [
       "Ex04c.mem",
@@ -28,7 +28,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "e3647e4503e1f7d5f5709ae0cce249f1"
+      "3c6c5014b5b6d2df90033c9525932354"
     ],
     [
       "Ex04c.append",
@@ -42,7 +42,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "03ddf381f958c627b302ca0653ba1ef6"
+      "b7c7ed93389f9038f199076c9d1d2edf"
     ],
     [
       "Ex04c.mem",
@@ -57,7 +57,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "858afa2dbde74d96d30b4aab138384ba"
+      "c3ba652c6b77c038abbd933f61f6e43f"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex04e.fst.hints b/doc/tutorial/code/exercises/Ex04e.fst.hints
@@ -8,7 +8,7 @@
       1,
       [ "@query" ],
       0,
-      "57956e1b8b706d4322e6925a60b61350"
+      "729a91124138f910db9a1efd79071a26"
     ],
     [
       "Ex04e.__proj__Some__item__v",
@@ -21,7 +21,7 @@
         "refinement_interpretation_Tm_refine_5940fa0a1398f97ef02a98908357b71e"
       ],
       0,
-      "b315d720a33120d95dbf09f389bfd535"
+      "5de54ec9ad823abc1fd0132d24f7c99e"
     ],
     [
       "Ex04e.find",
@@ -35,7 +35,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "51b503618545949bef9979988b7829cb"
+      "b6ec1265d3b76810e4c9567eaa337172"
     ],
     [
       "Ex04e.option",
@@ -44,7 +44,7 @@
       1,
       [ "@query" ],
       0,
-      "736fdd3c91d15983c1c7e00ab00914b1"
+      "a7a1a692fcfdd5e83bcd4bd7ff84a0b6"
     ],
     [
       "Ex04e.__proj__Some__item__v",
@@ -57,7 +57,7 @@
         "refinement_interpretation_Tm_refine_5940fa0a1398f97ef02a98908357b71e"
       ],
       0,
-      "37219efd4f8670dde8968594047cd800"
+      "8b0b8c71008a1efd6da95facfa3beb42"
     ],
     [
       "Ex04e.find",
@@ -71,7 +71,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "fbd0f2acfe84c989c8c89dcfbeda4d96"
+      "47c3a0f4db55c957afcd38c7f6618e66"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex04f.fst.hints b/doc/tutorial/code/exercises/Ex04f.fst.hints
@@ -14,7 +14,7 @@
         "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "3e5176c8901a92566f5f0e7a5a5cffba"
+      "e7d0f975c95284b7916443a001ce9714"
     ],
     [
       "Ex04f.reverse",
@@ -29,7 +29,7 @@
         "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "b30e7900ecdd662ae41a6558a55e498e"
+      "89f440dba4a1f1172085c14a6efc05f8"
     ],
     [
       "Ex04f.append",
@@ -43,7 +43,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "79cd04b67c11d9c0254976371623db42"
+      "ac835b16870cf7e8590a116c5f9afc33"
     ],
     [
       "Ex04f.reverse",
@@ -57,7 +57,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "63d4f2c24bce9ba5825fd809930ad020"
+      "c47b861f6861c46510e49cf7190e1e58"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex05a.fst.hints b/doc/tutorial/code/exercises/Ex05a.fst.hints
@@ -13,7 +13,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "c3aff04a331d3177ee6486a9602eebe6"
+      "8934826aeef963a5e138eaed678b2800"
     ],
     [
       "Ex05a.reverse",
@@ -27,7 +27,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "844b4a99303bcd55fc2cdf78cf8edba8"
+      "da1f06d2db27c18dd864a8baa58d4650"
     ],
     [
       "Ex05a.rev",
@@ -42,7 +42,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "081093c4774143e7a591097116b28c92"
+      "e67494f4891dbfcd9b58964cd602d578"
     ],
     [
       "Ex05a.append_assoc",
@@ -67,7 +67,7 @@
         "subterm_ordering_Prims.Cons", "typing_Ex05a.append"
       ],
       0,
-      "a932a62643e0e855d61e20ab2a3d760f"
+      "5b0d5f780c0b83337d274b9c2d72ddfd"
     ],
     [
       "Ex05a.append",
@@ -81,7 +81,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "9517727062eed914f6f4d767c30b5123"
+      "21471283c3b5c92d91ffef49251cf256"
     ],
     [
       "Ex05a.reverse",
@@ -95,7 +95,7 @@
         "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "f436c06fabbd6d8e217f23395331c91b"
+      "3b667f3113dda05fe78fc24953a5b948"
     ],
     [
       "Ex05a.rev",
@@ -110,7 +110,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "4e860fbb6f3af3a3387d3ad6a3ed8f73"
+      "dd31921f516e830950b1d3594f64d04d"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/Ex05b.fst.hints b/doc/tutorial/code/exercises/Ex05b.fst.hints
@@ -16,7 +16,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "2b63e36c76262bd1cb939acc302dcdf4"
+      "db55b0eb3bf4507d421f1b98325463e1"
     ],
     [
       "Ex05b.fib",
@@ -36,7 +36,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "f3ba4f442692f1b1383ebb7017535c1d"
+      "24be41bcd15cfe8e325a4089afe3c6de"
     ],
     [
       "Ex05b.fib_is_ok",
@@ -50,7 +50,7 @@
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
       ],
       0,
-      "eeeece88e4000172e33393c36d4eb1dc"
+      "8b47ab0f49b0bbfae1f80ff7e0d9a860"
     ],
     [
       "Ex05b.fibonacci",
@@ -67,7 +67,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "19afe142d4001b0e3044424d89beedf2"
+      "f3d15da6458296780984d9b8e86468f9"
     ],
     [
       "Ex05b.fib",
@@ -87,7 +87,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "4c86f5339e667005ca6ca9a2fee3b280"
+      "5a2fab5ae3358b80330c97423ad345d8"
     ],
     [
       "Ex05b.fib_is_ok",
@@ -101,7 +101,7 @@
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
       ],
       0,
-      "bac587a7992aa77170a2f6e1ef053cd5"
+      "3ca1281b397906415d307783454f5d83"
     ]
   ]
 ]