Merge pull request #507 from FStarLang/protz_numbered_enums

Add support internally for choosing the value of enum cases
FStarLang · Dec 20, 2024 · 4c619aa · 4c619aa
2 parents e0fe023 + 032fbda
commit 4c619aa
Show file tree

Hide file tree

Showing 26 changed files with 7,693 additions and 44 deletions.
diff --git a/krmllib/dist/generic/Makefile.include b/krmllib/dist/generic/Makefile.include
@@ -2,4 +2,4 @@ USER_TARGET=libkrmllib.a
 USER_CFLAGS=
 USER_C_FILES=c.c c_string.c fstar_bytes.c fstar_char.c fstar_date.c fstar_dyn.c fstar_hyperstack_io.c fstar_int16.c fstar_int32.c fstar_int64.c fstar_int8.c fstar_io.c fstar_string.c fstar_uint16.c fstar_uint32.c fstar_uint64.c fstar_uint8.c lowstar_printf.c prims.c testlib.c
 ALL_C_FILES=FStar_Order.c WasmSupport.c
-ALL_H_FILES=C.h C_Failure.h C_Loops.h C_String.h FStar_All.h FStar_BigOps.h FStar_BitVector.h FStar_Bytes.h FStar_Calc.h FStar_Char.h FStar_Date.h FStar_ErasedLogic.h FStar_Float.h FStar_FunctionalExtensionality.h FStar_GSet.h FStar_Heap.h FStar_HyperStack_All.h FStar_HyperStack_IO.h FStar_HyperStack_ST.h FStar_IO.h FStar_Int.h FStar_Int16.h FStar_Int32.h FStar_Int64.h FStar_Int8.h FStar_Int_Cast.h FStar_Issue.h FStar_Krml_Endianness.h FStar_List_Tot_Base.h FStar_List_Tot_Properties.h FStar_Map.h FStar_Math_Lib.h FStar_ModifiesGen.h FStar_Monotonic_Heap.h FStar_Monotonic_HyperHeap.h FStar_Monotonic_HyperStack.h FStar_Monotonic_Pure.h FStar_Mul.h FStar_Order.h FStar_Pervasives.h FStar_PredicateExtensionality.h FStar_Preorder.h FStar_ST.h FStar_Sealed_Inhabited.h FStar_Seq_Base.h FStar_Seq_Properties.h FStar_Set.h FStar_String.h FStar_TSet.h FStar_UInt.h FStar_UInt128.h FStar_UInt_8_16_32_64.h FStar_VConfig.h LowStar_Endianness.h LowStar_Monotonic_Buffer.h LowStar_Printf.h Prims.h TestLib.h WasmSupport.h
+ALL_H_FILES=C.h C_Failure.h C_Loops.h C_String.h FStar_All.h FStar_BigOps.h FStar_BitVector.h FStar_Bytes.h FStar_Calc.h FStar_Char.h FStar_Date.h FStar_ErasedLogic.h FStar_Float.h FStar_FunctionalExtensionality.h FStar_GSet.h FStar_Heap.h FStar_HyperStack_All.h FStar_HyperStack_IO.h FStar_HyperStack_ST.h FStar_IO.h FStar_Int.h FStar_Int16.h FStar_Int32.h FStar_Int64.h FStar_Int8.h FStar_Int_Cast.h FStar_Issue.h FStar_Krml_Endianness.h FStar_List_Tot_Base.h FStar_List_Tot_Properties.h FStar_Map.h FStar_Math_Lib.h FStar_ModifiesGen.h FStar_Monotonic_Heap.h FStar_Monotonic_HyperHeap.h FStar_Monotonic_HyperStack.h FStar_Monotonic_Pure.h FStar_Mul.h FStar_Order.h FStar_Pervasives.h FStar_Pprint.h FStar_PredicateExtensionality.h FStar_Preorder.h FStar_ST.h FStar_Sealed_Inhabited.h FStar_Seq_Base.h FStar_Seq_Properties.h FStar_Set.h FStar_String.h FStar_TSet.h FStar_UInt.h FStar_UInt128.h FStar_UInt_8_16_32_64.h LowStar_Endianness.h LowStar_Monotonic_Buffer.h LowStar_Printf.h Prims.h TestLib.h WasmSupport.h