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
Vale.Interop.Cast.fsti.hints
[
"S�(\u0012)EY��\u001b�sZ�`�",
[
[
"Vale.Interop.Cast.copy_down",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Interop.Types.TUInt8",
"constructor_distinct_Tm_unit",
"equality_tok_Interop.Types.TUInt8@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.min_int",
"equation_Interop.Base.base_typ_as_type",
"equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
"refinement_interpretation_Tm_refine_ff88a6ffa07bd660e3b3df07b89c350f",
"typing_Interop.Base.base_typ_as_type",
"typing_Interop.Types.view_n",
"typing_LowStar.Buffer.trivial_preorder"
],
0,
"bee0d2b33af0d5b12455dff9a010edc5"
],
[
"Vale.Interop.Cast.copy_imm_down",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Interop.Types.TUInt8",
"constructor_distinct_Tm_unit",
"equality_tok_Interop.Types.TUInt8@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Interop.Base.base_typ_as_type",
"equation_Interop.Types.view_n",
"equation_LowStar.ImmutableBuffer.ibuffer",
"equation_LowStar.ImmutableBuffer.immutable_preorder",
"equation_Prims.eqtype", "equation_Prims.nat", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
"refinement_interpretation_Tm_refine_f72b0c686d406abb3afa72e6a54839f6",
"typing_Interop.Base.base_typ_as_type",
"typing_Interop.Types.view_n",
"typing_LowStar.ImmutableBuffer.immutable_preorder"
],
0,
"af22811942afb1a151fa5d18b386f453"
],
[
"Vale.Interop.Cast.copy_up",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Interop.Types.TUInt8",
"constructor_distinct_Tm_unit",
"equality_tok_Interop.Types.TUInt8@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Interop.Base.base_typ_as_type",
"equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
"refinement_interpretation_Tm_refine_ff88a6ffa07bd660e3b3df07b89c350f",
"typing_Interop.Base.base_typ_as_type",
"typing_Interop.Types.view_n",
"typing_LowStar.Buffer.trivial_preorder"
],
0,
"ec4ac5bc120bbcf6512185850001b7cc"
],
[
"Vale.Interop.Cast.imm_copy_up",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Interop.Types.TUInt8",
"constructor_distinct_Tm_unit",
"equality_tok_Interop.Types.TUInt8@tok",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_Interop.Base.base_typ_as_type",
"equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_978d4c33025cd46e2dac7d50698e6899",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Interop.Base.base_typ_as_type",
"typing_Interop.Types.view_n",
"typing_LowStar.Buffer.trivial_preorder"
],
0,
"1c6e0e092c21068124d30c35f832116a"
],
[
"Vale.Interop.Cast.imm_copy_imm_up",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Interop.Types.TUInt8",
"constructor_distinct_Tm_unit",
"equality_tok_Interop.Types.TUInt8@tok",
"equation_FStar.UInt.min_int",
"equation_Interop.Base.base_typ_as_type",
"equation_Interop.Types.view_n",
"equation_LowStar.ImmutableBuffer.ibuffer", "equation_Prims.eqtype",
"equation_Prims.nat", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
"typing_Interop.Base.base_typ_as_type",
"typing_Interop.Types.view_n",
"typing_LowStar.ImmutableBuffer.immutable_preorder"
],
0,
"cd546fd522fd528029f1661d2f516d8d"
]
]
]
Computing file changes ...
