Revision 0f2ffb26900551cc06738230564b453820c1e87c authored by Dzomo the everest Yak on 01 April 2020, 08:20:26 UTC, committed by Dzomo the everest Yak on 01 April 2020, 08:20:26 UTC
1 parent 200ca29
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,
"5c9772ea2e5c2026f25add2f005f4886"
],
[
"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,
"1e7d53c306f314ff87ecc38cc3f6b40f"
],
[
"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,
"d87a6faa69c442e19f8cc128ef8d457a"
],
[
"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,
"865213cf0df91cef63cd062392a25550"
],
[
"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,
"778d64d04a7ebf51b603f80260913db7"
],
[
"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,
"a4f3334bc8e466c900882f546777e41c"
],
[
"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,
"75db49f330336f5bff6f1d4fb18d3f9b"
],
[
"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,
"6ecefd5e90c42917fa44483f02eb2fb0"
],
[
"Test.Lowstarize.__proj__LB__item__b",
1,
2,
1,
[
"@query", "proj_equation_Test.Lowstarize.LB_len",
"projection_inverse_Test.Lowstarize.LB_len"
],
0,
"fc37b7b6cf0e8ac6c4c9b260c63e577b"
],
[
"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,
"a909b3ae025069ca445e1199e6d84f42"
],
[
"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,
"ef2795a6a9b1dc65a17fdd419c2d3aeb"
],
[
"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,
"e4237eda9be1a08948f6122a5c50a5bc"
]
]
]
Computing file changes ...
