Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.Bignum.Defs.fsti.hints
[
"xQ��\t�㰈\u0018Y��\u0006�\u000f",
[
[
"Vale.Bignum.Defs.lemma_mul_div_n_lt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"331f18d3762a940c75f8f345215aeef2"
],
[
"Vale.Bignum.Defs.lemma_mul_div_n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"bfc7e02bb01cacd1c8ddf9f03eb901ba"
],
[
"Vale.Bignum.Defs.add_lo_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.natN",
"int_inversion", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"bff50baf3b4d0435aa30d843d6951dfc"
],
[
"Vale.Bignum.Defs.add_lo_hi",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9ff73c1c9198954a2c6204ae0d5d9b7e"
],
[
"Vale.Bignum.Defs.add_lo_hi",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"6391b45086487bbdc2d53564d177af72"
],
[
"Vale.Bignum.Defs.mul_lo_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"308acd4c70cd44aee451380cf6dce4af"
],
[
"Vale.Bignum.Defs.mul_lo_def",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"57f9e1a09358e99812fe2834e49dcc7e"
],
[
"Vale.Bignum.Defs.mul_lo",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a7e6a30d53cc6671396b3c0d2966b023"
],
[
"Vale.Bignum.Defs.reveal_mul_lo",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"1efddc5cca6fe02fde44f06678fad408"
],
[
"Vale.Bignum.Defs.reveal_mul_lo_all",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"f84a22a621571306a6871b80323af784"
],
[
"Vale.Bignum.Defs.mul_hi_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ec396ee4e15fae35529b164cc980a83a"
],
[
"Vale.Bignum.Defs.mul_hi_def",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c4e7fd073163507df52b99e95838fce4"
],
[
"Vale.Bignum.Defs.mul_hi",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0c5d5a2fa803a71ed8d930ab25de6bb3"
],
[
"Vale.Bignum.Defs.reveal_mul_hi",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"f3a4d3957334af5ed5d32dc54d5251cd"
],
[
"Vale.Bignum.Defs.reveal_mul_hi_all",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"a1be9a16ef3bc98faa9920b5a46bcb8f"
],
[
"Vale.Bignum.Defs.sum_seq_left",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"88421e78d588406f0e9d6a50e59aa88a"
],
[
"Vale.Bignum.Defs.sum_seq_right",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"0655127c39e182929d833fe10c793ac4"
],
[
"Vale.Bignum.Defs.pow_int",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"23063c326f645f881e1d087527a19b9e"
],
[
"Vale.Bignum.Defs.sum_pow_seq_left",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Bignum.Defs_interpretation_Tm_arrow_d5d333817377aec8da767181fea515e3",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Bignum.Defs.pow_seq",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"interpretation_Tm_abs_357cc5a6953c6fe391abcadab71ffd9b",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_357cc5a6953c6fe391abcadab71ffd9b",
"typing_Vale.Def.Words_s.natN"
],
0,
"35d4d42eb12695acaa7795a6166e062f"
],
[
"Vale.Bignum.Defs.sum_pow_seq",
1,
1,
0,
[ "@query" ],
0,
"3526d43868d0ebc413348e46bb017811"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...