Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
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,
"e6263d44ff29cab89d01b1e12811a313"
],
[
"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,
"7d359442ef95970681e9036321e3f43e"
],
[
"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,
"2c7bfbbbea1d7f699a1f30a2e9710a70"
],
[
"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,
"89f3db6da20e70ae8e4adb76797765a5"
],
[
"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,
"4ccbedd0711da700eb665f0385c18a52"
],
[
"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,
"ccabb6a1eb978c5fd84ca06b8c427660"
],
[
"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,
"29f35626927fd7f3f84910e0e9e80137"
],
[
"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,
"9b52210213d0f3e75d8b664c6385a109"
],
[
"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,
"f2f623c98aa1750202caf2723963b983"
],
[
"Test.Lowstarize.__proj__LB__item__b",
1,
2,
1,
[
"@query", "proj_equation_Test.Lowstarize.LB_len",
"projection_inverse_Test.Lowstarize.LB_len"
],
0,
"3679a3393aa2b693bdffb9c623b3f56e"
],
[
"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,
"523e07a93adc5bb15c7686addcb99ce3"
],
[
"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,
"f3d0900330b1284e9f75cb8ede550526"
],
[
"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,
"b0883b5729f02255cf82379893c7c86b"
]
]
]
Computing file changes ...
