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
Meta.Interface.fst.hints
[
"�z�ZZ��2\u000e:���鰙",
[
[
"Meta.Interface.assoc",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.assoc.fuel_instrumented",
"@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_with_fuel_FStar.List.Tot.Base.assoc.fuel_instrumented",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"typing_FStar.List.Tot.Base.assoc",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"7d3b977b52082f83aa23f4f517830996"
],
[
"Meta.Interface.__proj__Inline__item__new_name",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Meta.Interface.Inline",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_72d871bdf0e6e15cb9b70b8f1ef82b10"
],
0,
"12223cf188c49f4361b91e5ba98317dc"
],
[
"Meta.Interface.string_of_mapping",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Meta.Interface.Inline",
"disc_equation_Meta.Interface.Specialize",
"fuel_guarded_inversion_Meta.Interface.mapping"
],
0,
"cfc7779a752939e694fb809523651417"
],
[
"Meta.Interface.string_of_name",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "equation_FStar.Reflection.Types.name",
"fuel_guarded_inversion_Prims.list"
],
0,
"91e7d39956bf12c852ad952232f8a3c1"
],
[
"Meta.Interface.suffix_name",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "equation_FStar.Reflection.Types.name",
"fuel_guarded_inversion_Prims.list"
],
0,
"90dfdce509766efa0ca10845230b914c"
],
[
"Meta.Interface.in_namespace",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_20ccd379c93014ff7fe3312d7f024a43_0",
"binder_x_dce109b66917edb1ca83b9408101b740_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_FStar.Reflection.Types.name",
"fuel_guarded_inversion_Prims.list",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"subterm_ordering_Prims.Cons"
],
0,
"73765e2b28a72e3a91406fcc415d3a9c"
],
[
"Meta.Interface.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,
"261e78abdb536e500bf58f06bf2f95c1"
],
[
"Meta.Interface.visit_function",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Tactics.Result.Failed",
"constructor_distinct_FStar.Tactics.Result.Success",
"disc_equation_FStar.Pervasives.Native.None",
"fuel_guarded_inversion_FStar.Tactics.Result.__result",
"function_token_typing_FStar.Reflection.Types.sigelt",
"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,
"8aeb537584922f88abe2bc59bfc8d8f2"
],
[
"Meta.Interface.visit_function",
2,
2,
2,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.assoc.fuel_instrumented",
"@query",
"FStar.Reflection.Data_pretyping_ee655bc751cef679bca813f86c407d6b",
"Meta.Interface_pretyping_3687ebf883f49bee7aa0812c87d03fff",
"Prims_pretyping_ce036b6b736ef4e0bc3a9ff132a12aed",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Tactics.Result.Failed",
"constructor_distinct_FStar.Tactics.Result.Success",
"constructor_distinct_Meta.Interface.Specialize",
"data_elim_FStar.Tactics.Result.Success",
"data_elim_Meta.Interface.Mkstate",
"data_typing_intro_FStar.Reflection.Data.Tv_Unknown@tok",
"data_typing_intro_Meta.Interface.Specialize@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Reflection.Data.Tv_Abs",
"disc_equation_FStar.Reflection.Data.Tv_App",
"disc_equation_FStar.Reflection.Data.Tv_Arrow",
"disc_equation_FStar.Reflection.Data.Tv_AscribedC",
"disc_equation_FStar.Reflection.Data.Tv_AscribedT",
"disc_equation_FStar.Reflection.Data.Tv_BVar",
"disc_equation_FStar.Reflection.Data.Tv_Const",
"disc_equation_FStar.Reflection.Data.Tv_FVar",
"disc_equation_FStar.Reflection.Data.Tv_Let",
"disc_equation_FStar.Reflection.Data.Tv_Match",
"disc_equation_FStar.Reflection.Data.Tv_Refine",
"disc_equation_FStar.Reflection.Data.Tv_Type",
"disc_equation_FStar.Reflection.Data.Tv_Unknown",
"disc_equation_FStar.Reflection.Data.Tv_Uvar",
"disc_equation_FStar.Reflection.Data.Tv_Var",
"disc_equation_Meta.Interface.Inline",
"disc_equation_Meta.Interface.Specialize",
"equation_FStar.Reflection.Data.argv",
"equation_FStar.Reflection.Types.name", "equation_Prims.eqtype",
"fuel_guarded_inversion_FStar.Reflection.Data.term_view",
"fuel_guarded_inversion_FStar.Tactics.Result.__result",
"fuel_guarded_inversion_Meta.Interface.mapping",
"fuel_guarded_inversion_Meta.Interface.state",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_FStar.Reflection.Types.bv",
"function_token_typing_FStar.Reflection.Types.term",
"function_token_typing_Prims.bool",
"function_token_typing_Prims.string",
"kinding_FStar.Pervasives.Native.tuple4@tok",
"kinding_Meta.Interface.mapping@tok", "kinding_Prims.list@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Negation",
"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",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.List.Tot.Base.assoc",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Reflection.Basic.inspect_fv",
"typing_FStar.Reflection.Types.name",
"typing_Meta.Interface.__proj__Mkstate__item__seen", "unit_typing"
],
0,
"c2df2e3dcff0bb978183c09fc60c910f"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...