Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Test.Lowstarize.fst.hints
[
"\u001b>SY���S�G&1~b�",
[
[
"Test.Lowstarize.as_uint8s",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.for_all.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "FStar.Char_pretyping_dc6ef56115bc91878da75a1e0625bb73",
"FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250",
"Lib.Meta_interpretation_Tm_arrow_fc1554671c39653ed371206100dcafd3",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_BoxBool",
"constructor_distinct_FStar.Tactics.Result.Failed",
"constructor_distinct_FStar.Tactics.Result.Success",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Tactics.Result.__result",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Lib.Meta.is_hex_digit",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_Modulus", "proj_equation_Prims.Cons_tl",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Tactics.Result.Failed_a",
"projection_inverse_FStar.Tactics.Result.Failed_exn",
"projection_inverse_FStar.Tactics.Result.Failed_ps",
"projection_inverse_FStar.Tactics.Result.Success_a",
"projection_inverse_FStar.Tactics.Result.Success_ps",
"projection_inverse_FStar.Tactics.Result.Success_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
"refinement_interpretation_Tm_refine_b338ec010a48764c17c429acaf5dcd17",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"token_correspondence_Lib.Meta.is_hex_digit",
"typing_FStar.Char.char", "typing_Lib.Meta.is_hex_digit",
"typing_Prims.__proj__Cons__item__tl"
],
0,
"43aecf87c6ed3bf45d22e342300d8c3f"
],
[
"Test.Lowstarize.is_some",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"f505e855dcaf994a6f47bd285b10a867"
],
[
"Test.Lowstarize.must",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"2ae4823eaea043ea725a3a43198251e4"
],
[
"Test.Lowstarize.destruct_list",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Reflection.Types.name", "equation_Prims.eqtype",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Reflection.Types.name"
],
0,
"603cc5fc5287d12ec15f9f7804117d3f"
],
[
"Test.Lowstarize.is_list",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Reflection.Types.name", "equation_Prims.eqtype",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Reflection.Types.name"
],
0,
"6cd6736a3344b99625c69cc7d03b7156"
],
[
"Test.Lowstarize.destruct_tuple",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"assumption_Prims.list__uu___haseq", "equation_Prims.eqtype",
"function_token_typing_Prims.string",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"85c2b2cb264b8cf2bd98ef81db2fda80"
],
[
"Test.Lowstarize.is_tuple",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"assumption_Prims.list__uu___haseq", "equation_Prims.eqtype",
"function_token_typing_Prims.string",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"af837b01f4d6da0d894d9aae7b06e6b6"
],
[
"Test.Lowstarize.destruct_hex",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons",
"equation_FStar.Reflection.Data.argv", "equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_FStar.Reflection.Data.argv", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.List.Tot.Base.length"
],
0,
"24e93c751d4f480b5a098eafe161a8f7"
],
[
"Test.Lowstarize.fresh",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Tactics.Result.Success",
"equation_FStar.Pervasives.Native.snd",
"equation_FStar.Reflection.Types.name", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Test.Lowstarize.gensym",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_FStar.Tactics.Result.__result",
"function_token_typing_Prims.string", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Tactics.Result.Success_a",
"projection_inverse_FStar.Tactics.Result.Success_ps",
"projection_inverse_FStar.Tactics.Result.Success_v",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Pervasives.Native.snd"
],
0,
"9f34326fd21d6ecc865ee7febeb4de51"
],
[
"Test.Lowstarize.__proj__LB__item__b",
1,
2,
1,
[
"@query", "proj_equation_Test.Lowstarize.LB_len",
"projection_inverse_Test.Lowstarize.LB_len"
],
0,
"f7ab7e15dd12b494f506c1dbaf7cd16a"
],
[
"Test.Lowstarize.mk_gcmalloc_of_list",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"FStar.Reflection.Data_pretyping_ee655bc751cef679bca813f86c407d6b",
"bool_inversion", "constructor_distinct_FStar.Tactics.Result.Failed",
"constructor_distinct_FStar.Tactics.Result.Success",
"data_typing_intro_FStar.Reflection.Data.Tv_Unknown@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Test.Lowstarize.gensym",
"fuel_guarded_inversion_FStar.Tactics.Result.__result",
"function_token_typing_FStar.Reflection.Types.term",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Tactics.Result.Failed_a",
"projection_inverse_FStar.Tactics.Result.Failed_exn",
"projection_inverse_FStar.Tactics.Result.Failed_ps",
"projection_inverse_FStar.Tactics.Result.Success_a",
"projection_inverse_FStar.Tactics.Result.Success_ps",
"projection_inverse_FStar.Tactics.Result.Success_v",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"742ad1e707a4b9f16627fa990169eae2"
],
[
"Test.Lowstarize.lowstarize_hex",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.for_all.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250",
"Lib.Meta_interpretation_Tm_arrow_fc1554671c39653ed371206100dcafd3",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Tm_unit", "equation_FStar.String.char",
"equation_FStar.String.strlen", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Lib.Meta.is_hex_digit",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Negation", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Lib.Meta.is_hex_digit",
"typing_FStar.Char.char", "typing_FStar.List.Tot.Base.for_all",
"typing_FStar.String.list_of_string", "typing_FStar.String.strlen"
],
0,
"2c565785a0735d61fb7098edff651b7f"
],
[
"Test.Lowstarize.lowstarize_expr",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Tactics.Result.Failed",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Test.Lowstarize.gensym",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_FStar.Tactics.Result.__result",
"function_token_typing_FStar.Reflection.Types.sigelt",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_FStar.Tactics.Result.Failed_a",
"projection_inverse_FStar.Tactics.Result.Failed_exn",
"projection_inverse_FStar.Tactics.Result.Failed_ps",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"bfcc368ed150a5462c8d99ec7ebab3c9"
]
]
]
Computing file changes ...
