Merge pull request #3080 from mtzguido/misc1

misc: A fix and a new function
FStarLang · Nov 2, 2023 · 428cd65 · 428cd65
2 parents ea917da + 6429b09
commit 428cd65
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 0 deletions.
diff --git a/ocaml/fstar-lib/FStar_Sealed.ml b/ocaml/fstar-lib/FStar_Sealed.ml
@@ -1,2 +1,4 @@
 type 'a sealed = 'a
 let seal x = x
+let map_seal s f = f s
+let bind_seal s f = f s
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Derived.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Derived.ml
diff --git a/ulib/FStar.Reflection.V2.Derived.fst b/ulib/FStar.Reflection.V2.Derived.fst
@@ -114,6 +114,11 @@ let rec mk_tot_arr_ln (bs: list binder) (cod : term) : Tot term (decreases bs) =
     | [] -> cod
     | (b::bs) -> pack_ln (Tv_Arrow b (pack_comp (C_Total (mk_tot_arr_ln bs cod))))
 
+let rec mk_arr_ln (bs: list binder{~(Nil? bs)}) (cod : comp) : Tot term (decreases bs) =
+    match bs with
+    | [b] -> pack_ln (Tv_Arrow b cod)
+    | (b::bs) -> pack_ln (Tv_Arrow b (pack_comp (C_Total (mk_arr_ln bs cod))))
+
 let rec collect_arr' (bs : list binder) (c : comp) : Tot (list binder * comp) (decreases c) =
     begin match inspect_comp c with
     | C_Total t ->