From 84eecc4f73db98ee4cb40d373cfa3cac5e419c23 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 23 Oct 2024 12:14:30 -0700 Subject: [PATCH 1/2] remove duplicate lowercase hint files they cause trouble on Windows, since they are collapsed into one single file, and then git reports a dirty state, which blocks the EverParse release on Windows. --- examples/metatheory/indind.fst.hints | 646 ---------------------- examples/rel/label.fst.hints | 24 - examples/termination/mcCarthy91.fst.hints | 57 -- ulib/.hints/prims.fst.hints | 85 --- 4 files changed, 812 deletions(-) delete mode 100644 examples/metatheory/indind.fst.hints delete mode 100644 examples/rel/label.fst.hints delete mode 100644 examples/termination/mcCarthy91.fst.hints delete mode 100644 ulib/.hints/prims.fst.hints diff --git a/examples/metatheory/indind.fst.hints b/examples/metatheory/indind.fst.hints deleted file mode 100644 index 15025c1fadb..00000000000 --- a/examples/metatheory/indind.fst.hints +++ /dev/null @@ -1,646 +0,0 @@ -[ - "YG\u0007A`", - [ - [ - "Indind.vdl0", - 1, - 2, - 1, - [ "@query" ], - 0, - "48135a49c8a7c5615b1b07d161778dcb" - ], - [ - "Indind.__proj__Cons__item__tail", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_f2b0a695d9cf05c47cf3e9edd0a8491e" - ], - 0, - "23204934cfbfa3743b786a13c6d20a90" - ], - [ - "Indind.__proj__Cons__item___1", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_f2b0a695d9cf05c47cf3e9edd0a8491e" - ], - 0, - "f1ca0d8c873a673a77414b0d6597b341" - ], - [ - "Indind.__proj__S__item__l", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_2a5da96b896242ec4724a0edc1956d4a" - ], - 0, - "1fc6631cafe2863c051f01aa3bf66fc7" - ], - [ - "Indind.__proj__S__item__x", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_2a5da96b896242ec4724a0edc1956d4a" - ], - 0, - "c0a4f7f4dc4b7d1b4cd56217207543d3" - ], - [ - "Indind.vdl_valid", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Indind_pretyping_c036994c42c57d1c399c8bad9fcec1c8", - "Indind_pretyping_e6826aca16e75f7cd623b3f84232824b", - "binder_x_c036994c42c57d1c399c8bad9fcec1c8_0", - "disc_equation_Indind.Cons", "disc_equation_Indind.Nil", - "equality_tok_Indind.Nil@tok", "equality_tok_Indind.Z@tok", - "fuel_guarded_inversion_Indind.vdl0", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Indind.Cons", - "typing_tok_Indind.Nil@tok", "typing_tok_Indind.Z@tok" - ], - 0, - "ee41976787e79d11867393db3bd46168" - ], - [ - "Indind.vdl_valid", - 2, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Indind_pretyping_c036994c42c57d1c399c8bad9fcec1c8", - "Indind_pretyping_e6826aca16e75f7cd623b3f84232824b", - "binder_x_e6826aca16e75f7cd623b3f84232824b_1", - "disc_equation_Indind.S", "disc_equation_Indind.Z", - "equality_tok_Indind.Nil@tok", "equality_tok_Indind.Z@tok", - "fuel_guarded_inversion_Indind.content0", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Indind.S", - "typing_tok_Indind.Nil@tok", "typing_tok_Indind.Z@tok" - ], - 0, - "3460dc72915b443b784c889e6943dec6" - ], - [ - "Indind.vdl_induction", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.content_valid.fuel_instrumented", - "@fuel_correspondence_Indind.vdl_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.content_valid.fuel_instrumented", "@query", - "Indind_pretyping_c036994c42c57d1c399c8bad9fcec1c8", - "binder_x_9deb54e5638969c5c40d598c80f71413_6", - "constructor_distinct_Indind.Cons", - "constructor_distinct_Indind.Nil", "disc_equation_Indind.Cons", - "disc_equation_Indind.Nil", "eq2-interp", - "equality_tok_Indind.Nil@tok", "equation_Indind.vdl", - "equation_with_fuel_Indind.content_valid.fuel_instrumented", - "equation_with_fuel_Indind.vdl_valid.fuel_instrumented", - "fuel_guarded_inversion_Indind.content0", - "fuel_guarded_inversion_Indind.vdl0", "l_and-interp", - "projection_inverse_BoxBool_proj_0", - "projection_inverse_Indind.Cons__1", - "projection_inverse_Indind.Cons_tail", - "refinement_interpretation_Tm_refine_d9f60de369feca465a8f4b9fd97b1a06", - "subterm_ordering_Indind.Cons", "true_interp", - "typing_tok_Indind.Nil@tok" - ], - 0, - "a54688813edc89ba8957975c70922205" - ], - [ - "Indind.vdl_induction", - 2, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.content_valid.fuel_instrumented", - "@fuel_correspondence_Indind.vdl_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.content_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.vdl_valid.fuel_instrumented", "@query", - "Indind_pretyping_c036994c42c57d1c399c8bad9fcec1c8", - "binder_x_9deb54e5638969c5c40d598c80f71413_6", - "binder_x_e5a1e0108979f3214409b56f719f3a62_7", - "constructor_distinct_Indind.S", "constructor_distinct_Indind.Z", - "disc_equation_Indind.S", "disc_equation_Indind.Z", "eq2-interp", - "equality_tok_Indind.Nil@tok", "equality_tok_Indind.Z@tok", - "equation_Indind.content", "equation_Indind.vdl", - "equation_with_fuel_Indind.content_valid.fuel_instrumented", - "fuel_guarded_inversion_Indind.content0", "l_and-interp", - "projection_inverse_BoxBool_proj_0", "projection_inverse_Indind.S_l", - "projection_inverse_Indind.S_x", - "refinement_interpretation_Tm_refine_7ebdb731056e76c249303fc299c05048", - "refinement_interpretation_Tm_refine_d9f60de369feca465a8f4b9fd97b1a06", - "subterm_ordering_Indind.Cons", "typing_tok_Indind.Nil@tok" - ], - 0, - "9cdc1c81eae7caff278118c02bab5d7b" - ], - [ - "Indind.vdl_induction", - 3, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.content_valid.fuel_instrumented", - "@fuel_correspondence_Indind.vdl_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.content_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.vdl_valid.fuel_instrumented", "@query", - "Indind_pretyping_c036994c42c57d1c399c8bad9fcec1c8", - "constructor_distinct_Indind.Cons", - "constructor_distinct_Indind.Nil", "constructor_distinct_Indind.S", - "constructor_distinct_Indind.Z", "data_typing_intro_Indind.Cons@tok", - "data_typing_intro_Indind.S@tok", "eq2-interp", - "equality_tok_Indind.Nil@tok", "equality_tok_Indind.Z@tok", - "equation_Indind.content", "equation_Indind.vdl", - "equation_with_fuel_Indind.content_valid.fuel_instrumented", - "equation_with_fuel_Indind.vdl_valid.fuel_instrumented", - "fuel_guarded_inversion_Indind.vdl0", "l_and-interp", - "projection_inverse_Indind.Cons__1", - "projection_inverse_Indind.Cons_tail", - "projection_inverse_Indind.S_l", "projection_inverse_Indind.S_x", - "refinement_interpretation_Tm_refine_7ebdb731056e76c249303fc299c05048", - "refinement_interpretation_Tm_refine_d9f60de369feca465a8f4b9fd97b1a06", - "true_interp", "typing_tok_Indind.Nil@tok", "typing_tok_Indind.Z@tok" - ], - 0, - "13391be7548bfd272faa1dba95c971cf" - ], - [ - "Indind.ctx0", - 1, - 2, - 1, - [ "@query" ], - 0, - "7661b1754851956c829c927983379c0b" - ], - [ - "Indind.__proj__ConsCtx__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_e3baa197ad5eea1780d7a86146099756" - ], - 0, - "cf6b5485ef65d6df1fb25ab15b3bb5f0" - ], - [ - "Indind.__proj__ConsCtx__item__a", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_e3baa197ad5eea1780d7a86146099756" - ], - 0, - "96f9d2bda8d083717a6a573849334d0f" - ], - [ - "Indind.__proj__Unit__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0dc85a3677e9bc75ef37439f19783424" - ], - 0, - "2a016fd13458b5af23b7fce4bc3e4446" - ], - [ - "Indind.__proj__Bool__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_ea431236476936535bf46955fedbfdc2" - ], - 0, - "4c2d3ea9230db982b5905a2a88da1439" - ], - [ - "Indind.__proj__Prod__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3c79ee0fccfffabe0477a0ac05c33065" - ], - 0, - "c5200074a0d4e24ab374a23d113d2c67" - ], - [ - "Indind.__proj__Prod__item__a", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3c79ee0fccfffabe0477a0ac05c33065" - ], - 0, - "da9b90596d067aece1ecb637d0f4e1cf" - ], - [ - "Indind.__proj__Prod__item__b", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3c79ee0fccfffabe0477a0ac05c33065" - ], - 0, - "85e4f8b72ac225c3d835c0de8531220f" - ], - [ - "Indind.__proj__U__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0443c2448a0ac6491f3d06f4a4d5008d" - ], - 0, - "bd33018458617c88130e7625ae411ee5" - ], - [ - "Indind.__proj__Var__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_caae48ea10f3641ef7ea72ad50f19db4" - ], - 0, - "6f2f5fc0806dd0630d82a8e730dd80b3" - ], - [ - "Indind.__proj__Var__item___1", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_caae48ea10f3641ef7ea72ad50f19db4" - ], - 0, - "fa6ceab84314a0ef5da16da33bb80c48" - ], - [ - "Indind.__proj__UHere__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_6d034f126c626bc9c0962d683e6b9995" - ], - 0, - "ae1b9665257b24a03c3faeb48e0fc513" - ], - [ - "Indind.__proj__UNext__item__g", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_696eac43ea98aadff1ccb166db0c0ee6" - ], - 0, - "014a7e75226f09bbb24fe7a3ea37d0af" - ], - [ - "Indind.__proj__UNext__item__a", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_696eac43ea98aadff1ccb166db0c0ee6" - ], - 0, - "bfaa97b896b9661ecc4cc3d052e93879" - ], - [ - "Indind.__proj__UNext__item___2", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_696eac43ea98aadff1ccb166db0c0ee6" - ], - 0, - "0f026f778b79b11ad4098d72f982cc45" - ], - [ - "Indind.ctx_valid", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Indind_pretyping_410c5fca59e32611bb891731d6f7b979", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "binder_x_88020d788a1a1b769f6a0274facda102_0", - "disc_equation_Indind.ConsCtx", "disc_equation_Indind.EmptyCtx", - "equality_tok_Indind.EmptyCtx@tok", - "fuel_guarded_inversion_Indind.ctx0", - "projection_inverse_BoxBool_proj_0", - "subterm_ordering_Indind.ConsCtx", "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "cd017cd53407a67ce497cedefd0c5a60" - ], - [ - "Indind.ctx_valid", - 2, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Indind_pretyping_410c5fca59e32611bb891731d6f7b979", - "Indind_pretyping_533aa6259d08b9168dde2184ec776f4d", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "binder_x_410c5fca59e32611bb891731d6f7b979_0", - "disc_equation_Indind.Bool", "disc_equation_Indind.Prod", - "disc_equation_Indind.U", "disc_equation_Indind.Unit", - "disc_equation_Indind.Var", "equality_tok_Indind.EmptyCtx@tok", - "fuel_guarded_inversion_Indind.valid_typ0", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Indind.Bool", - "subterm_ordering_Indind.Prod", "subterm_ordering_Indind.U", - "subterm_ordering_Indind.Unit", "subterm_ordering_Indind.Var", - "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "496a799a57d30bf494bf52f21e4cbe78" - ], - [ - "Indind.ctx_valid", - 3, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Indind_pretyping_410c5fca59e32611bb891731d6f7b979", - "Indind_pretyping_533aa6259d08b9168dde2184ec776f4d", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "binder_x_533aa6259d08b9168dde2184ec776f4d_0", - "disc_equation_Indind.UHere", "disc_equation_Indind.UNext", - "equality_tok_Indind.EmptyCtx@tok", - "fuel_guarded_inversion_Indind.u_mem0", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Indind.UHere", - "subterm_ordering_Indind.UNext", "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "f382953964b490344775aa94adf55867" - ], - [ - "Indind.empty_ctx", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", "@query", - "constructor_distinct_Indind.EmptyCtx", - "equality_tok_Indind.EmptyCtx@tok", - "equation_with_fuel_Indind.ctx_valid.fuel_instrumented", - "true_interp", "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "0762fed4527d9b18e1c6528e629392c0" - ], - [ - "Indind.cons_ctx", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.valid_typ_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.valid_typ_valid.fuel_instrumented", - "@query", "constructor_distinct_Indind.ConsCtx", - "data_typing_intro_Indind.ConsCtx@tok", "equation_Indind.ctx", - "equation_Indind.valid_typ", - "equation_with_fuel_Indind.ctx_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.ConsCtx_a", - "projection_inverse_Indind.ConsCtx_g", - "refinement_interpretation_Tm_refine_699266a0694fa43def73d31629b96e97", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96" - ], - 0, - "9ba92ef6ba18ad681205e928735c7ae1" - ], - [ - "Indind.unit", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.valid_typ_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", "@query", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "constructor_distinct_Indind.Unit", - "data_typing_intro_Indind.Unit@tok", "eq2-interp", - "equality_tok_Indind.EmptyCtx@tok", "equation_Indind.ctx", - "equation_with_fuel_Indind.valid_typ_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.Unit_g", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96", - "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "6e2a5db64a9f5972bad3659107744103" - ], - [ - "Indind.bool", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.valid_typ_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", "@query", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "constructor_distinct_Indind.Bool", - "data_typing_intro_Indind.Bool@tok", "eq2-interp", - "equality_tok_Indind.EmptyCtx@tok", "equation_Indind.ctx", - "equation_with_fuel_Indind.valid_typ_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.Bool_g", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96", - "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "2546a161cf34ddb25449ac377818b754" - ], - [ - "Indind.prod", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.valid_typ_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.valid_typ_valid.fuel_instrumented", - "@query", "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "constructor_distinct_Indind.Prod", - "data_typing_intro_Indind.Prod@tok", "eq2-interp", - "equality_tok_Indind.EmptyCtx@tok", "equation_Indind.cons_ctx", - "equation_Indind.ctx", "equation_Indind.valid_typ", - "equation_with_fuel_Indind.ctx_valid.fuel_instrumented", - "equation_with_fuel_Indind.valid_typ_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.Prod_a", - "projection_inverse_Indind.Prod_b", - "projection_inverse_Indind.Prod_g", - "refinement_interpretation_Tm_refine_699266a0694fa43def73d31629b96e97", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96", - "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "39c85f83fe1d9febd4839fc29b91f8ca" - ], - [ - "Indind.u", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.valid_typ_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", "@query", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "constructor_distinct_Indind.U", "data_typing_intro_Indind.U@tok", - "eq2-interp", "equality_tok_Indind.EmptyCtx@tok", - "equation_Indind.ctx", - "equation_with_fuel_Indind.valid_typ_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.U_g", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96", - "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "64cf894b3962733a4fc7d4bcd90a0ee2" - ], - [ - "Indind.var", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.u_mem_valid.fuel_instrumented", - "@fuel_correspondence_Indind.valid_typ_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.u_mem_valid.fuel_instrumented", "@query", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "constructor_distinct_Indind.Var", - "data_typing_intro_Indind.Var@tok", "eq2-interp", - "equality_tok_Indind.EmptyCtx@tok", "equation_Indind.ctx", - "equation_Indind.u_mem", - "equation_with_fuel_Indind.valid_typ_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.Var__1", - "projection_inverse_Indind.Var_g", - "refinement_interpretation_Tm_refine_e32bccd1293d964d651577ee7f1895e2", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96", - "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "f0b80b1ccaa58360b4e4ed6bef84bceb" - ], - [ - "Indind.u_here", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.u_mem_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", "@query", - "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "constructor_distinct_Indind.UHere", - "data_typing_intro_Indind.UHere@tok", "eq2-interp", - "equality_tok_Indind.EmptyCtx@tok", "equation_Indind.cons_ctx", - "equation_Indind.ctx", "equation_Indind.u", - "equation_with_fuel_Indind.u_mem_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.UHere_g", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96", - "typing_Indind.cons_ctx", "typing_Indind.u", - "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "114a48ccc3e4f421011f727ecac1c42c" - ], - [ - "Indind.u_next", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Indind.ctx_valid.fuel_instrumented", - "@fuel_correspondence_Indind.u_mem_valid.fuel_instrumented", - "@fuel_correspondence_Indind.valid_typ_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.ctx_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.u_mem_valid.fuel_instrumented", - "@fuel_irrelevance_Indind.valid_typ_valid.fuel_instrumented", - "@query", "Indind_pretyping_88020d788a1a1b769f6a0274facda102", - "constructor_distinct_Indind.UNext", - "data_typing_intro_Indind.UNext@tok", "eq2-interp", - "equality_tok_Indind.EmptyCtx@tok", "equation_Indind.cons_ctx", - "equation_Indind.ctx", "equation_Indind.u_mem", - "equation_Indind.valid_typ", - "equation_with_fuel_Indind.ctx_valid.fuel_instrumented", - "equation_with_fuel_Indind.u_mem_valid.fuel_instrumented", - "equation_with_fuel_Indind.valid_typ_valid.fuel_instrumented", - "l_and-interp", "projection_inverse_Indind.UNext__2", - "projection_inverse_Indind.UNext_a", - "projection_inverse_Indind.UNext_g", - "refinement_interpretation_Tm_refine_699266a0694fa43def73d31629b96e97", - "refinement_interpretation_Tm_refine_e32bccd1293d964d651577ee7f1895e2", - "refinement_interpretation_Tm_refine_f441914d47c90ea32f27f2a05474ce96", - "typing_Indind.cons_ctx", "typing_tok_Indind.EmptyCtx@tok" - ], - 0, - "7cdfdacbb95454e00b9fa3c7af916cbd" - ] - ] -] \ No newline at end of file diff --git a/examples/rel/label.fst.hints b/examples/rel/label.fst.hints deleted file mode 100644 index fd06ac23b81..00000000000 --- a/examples/rel/label.fst.hints +++ /dev/null @@ -1,24 +0,0 @@ -[ - "_|OSF5 Date: Wed, 23 Oct 2024 12:51:07 -0700 Subject: [PATCH 2/2] Removing more stale hints by .scripts/remove_stale_hints.sh --- examples/dm4free/delimcc.fst.hints | 121 --- ...AndNonStrictlyPositiveinductives.fst.hints | 107 -- examples/termination/maxime.fst.hints | 1 - examples/termination/termination.fst.hints | 438 -------- ulib/.hints/FStar.All.fst.hints | 17 - ulib/.hints/FStar.BaseTypes.fsti.hints | 1 - ulib/.hints/FStar.IO.fst.hints | 1 - .../FStar.Reflection.V1.Builtins.fsti.hints | 1 - .../FStar.Reflection.V1.Data.fsti.hints | 955 ------------------ .../FStar.Reflection.V2.Builtins.fsti.hints | 1 - .../FStar.Reflection.V2.Data.fsti.hints | 931 ----------------- ulib/.hints/FStar.Stubs.Pprint.fsti.hints | 1 - ulib/.hints/FStar.Tactics.Common.fst.hints | 17 - ulib/.hints/FStar.Tactics.Common.fsti.hints | 17 - ulib/.hints/FStar.Tactics.Result.fst.hints | 76 -- ulib/.hints/FStar.Tactics.Types.fsti.hints | 1 - ulib/.hints/FStar.Tactics.Unseal.fsti.hints | 1 - ulib/.hints/FStar.Tactics.V1.fst.hints | 1 - ulib/.hints/FStar.Tactics.V2.fst.hints | 1 - ulib/.hints/FStar.Tactics.fst.hints | 1 - ulib/.hints/FStar.VConfig.fsti.hints | 21 - 21 files changed, 2711 deletions(-) delete mode 100644 examples/dm4free/delimcc.fst.hints delete mode 100644 examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst.hints delete mode 100644 examples/termination/maxime.fst.hints delete mode 100644 examples/termination/termination.fst.hints delete mode 100644 ulib/.hints/FStar.All.fst.hints delete mode 100644 ulib/.hints/FStar.BaseTypes.fsti.hints delete mode 100644 ulib/.hints/FStar.IO.fst.hints delete mode 100644 ulib/.hints/FStar.Reflection.V1.Builtins.fsti.hints delete mode 100644 ulib/.hints/FStar.Reflection.V1.Data.fsti.hints delete mode 100644 ulib/.hints/FStar.Reflection.V2.Builtins.fsti.hints delete mode 100644 ulib/.hints/FStar.Reflection.V2.Data.fsti.hints delete mode 100644 ulib/.hints/FStar.Stubs.Pprint.fsti.hints delete mode 100644 ulib/.hints/FStar.Tactics.Common.fst.hints delete mode 100644 ulib/.hints/FStar.Tactics.Common.fsti.hints delete mode 100644 ulib/.hints/FStar.Tactics.Result.fst.hints delete mode 100644 ulib/.hints/FStar.Tactics.Types.fsti.hints delete mode 100644 ulib/.hints/FStar.Tactics.Unseal.fsti.hints delete mode 100644 ulib/.hints/FStar.Tactics.V1.fst.hints delete mode 100644 ulib/.hints/FStar.Tactics.V2.fst.hints delete mode 100644 ulib/.hints/FStar.Tactics.fst.hints delete mode 100644 ulib/.hints/FStar.VConfig.fsti.hints diff --git a/examples/dm4free/delimcc.fst.hints b/examples/dm4free/delimcc.fst.hints deleted file mode 100644 index c03415c33fa..00000000000 --- a/examples/dm4free/delimcc.fst.hints +++ /dev/null @@ -1,121 +0,0 @@ -[ - "o|l\u00123iw", - [ - [ - "DelimCC.right_unit", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_DelimCC.bind_k", - "equation_DelimCC.kont", "equation_DelimCC.return_k", - "equation_FStar.FunctionalExtensionality.feq", - "interpretation_Tm_abs_1375cdca81f1057e5eda83d9ff43a016", - "interpretation_Tm_abs_aad36e2eedb2945785e00c618a25bba1", - "interpretation_Tm_abs_dbc241f45b0c6f5a341c51802caa5547", - "refinement_interpretation_Tm_refine_84bbb68e2555b186061c13809014564f", - "token_correspondence_DelimCC.return_k", - "typing_Tm_abs_dbc241f45b0c6f5a341c51802caa5547" - ], - 0, - "1efa3aab038adf36a9635d185a7bf9c2" - ], - [ - "DelimCC.left_unit", - 1, - 2, - 1, - [ - "@query", "equation_DelimCC.bind_k", "equation_DelimCC.return_k", - "equation_FStar.FunctionalExtensionality.feq", - "interpretation_Tm_abs_1375cdca81f1057e5eda83d9ff43a016", - "interpretation_Tm_abs_aad36e2eedb2945785e00c618a25bba1", - "interpretation_Tm_abs_dbc241f45b0c6f5a341c51802caa5547" - ], - 0, - "1c977eab28ac2159e14d558dac106f9e" - ], - [ - "DelimCC.associativity", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_DelimCC.bind_k", - "equation_DelimCC.kont", - "equation_FStar.FunctionalExtensionality.feq", - "interpretation_Tm_abs_1375cdca81f1057e5eda83d9ff43a016", - "interpretation_Tm_abs_8fb38370c43370cf173b331103352a1e", - "interpretation_Tm_abs_dbc241f45b0c6f5a341c51802caa5547", - "refinement_interpretation_Tm_refine_84bbb68e2555b186061c13809014564f", - "typing_Tm_abs_dbc241f45b0c6f5a341c51802caa5547" - ], - 0, - "ac86856b64818ab95111f3cfd881c682" - ], - [ - "DelimCC.right_unit2", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_DelimCC.bind_k2", - "equation_DelimCC.kont2", "equation_DelimCC.return_k2", - "equation_FStar.FunctionalExtensionality.feq", - "interpretation_Tm_abs_0de330fc678989ce5861c85495562e0c", - "interpretation_Tm_abs_1e3b98a86efe10c813341778f12f9d1b", - "interpretation_Tm_abs_a210d7a9f583a6ace87f21677d0e5051", - "refinement_interpretation_Tm_refine_08d98d1a6a9f5eaedb943ec6a353e610", - "token_correspondence_DelimCC.return_k2", - "typing_Tm_abs_a210d7a9f583a6ace87f21677d0e5051" - ], - 0, - "d4f05635f191703cf97028c0c6316db0" - ], - [ - "DelimCC.left_unit2", - 1, - 2, - 1, - [ - "@query", "equation_DelimCC.bind_k2", "equation_DelimCC.return_k2", - "equation_FStar.FunctionalExtensionality.feq", - "interpretation_Tm_abs_0de330fc678989ce5861c85495562e0c", - "interpretation_Tm_abs_1e3b98a86efe10c813341778f12f9d1b", - "interpretation_Tm_abs_a210d7a9f583a6ace87f21677d0e5051" - ], - 0, - "846b13bbe33854347b7a1c977b203ee5" - ], - [ - "DelimCC.associativity2", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_DelimCC.bind_k2", - "equation_DelimCC.kont2", - "equation_FStar.FunctionalExtensionality.feq", - "interpretation_Tm_abs_0de330fc678989ce5861c85495562e0c", - "interpretation_Tm_abs_4e59e68fcdad5d80a4fa17c66d2981b9", - "interpretation_Tm_abs_a210d7a9f583a6ace87f21677d0e5051", - "refinement_interpretation_Tm_refine_08d98d1a6a9f5eaedb943ec6a353e610", - "typing_Tm_abs_a210d7a9f583a6ace87f21677d0e5051" - ], - 0, - "917972a1c99c3489214c9435f4d1497f" - ], - [ - "DelimCC.left_unit3", - 1, - 2, - 1, - [ - "@query", "equation_FStar.FunctionalExtensionality.feq", - "interpretation_Tm_abs_dbdc705d0aa12bf03732867b4b6d0795" - ], - 0, - "704f5b5121b8fe100cfd1bc7d918edef" - ] - ] -] \ No newline at end of file diff --git a/examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst.hints b/examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst.hints deleted file mode 100644 index 83f7ad07d65..00000000000 --- a/examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst.hints +++ /dev/null @@ -1,107 +0,0 @@ -[ - "MU4\u001dZ6&D", - [ - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.inj", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.eq2", - "equation_Prims.squash", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", - "unit_inversion" - ], - 0, - "b15b70f718c1f702fa45f14c90e34f9c" - ], - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.inj_injective", - 1, - 2, - 1, - [ - "@query", "eq2-interp", - "equation_PropImpredicativeAndNonStrictlyPositiveInductives.inj", - "interpretation_Tm_abs_9951d8bbbf25b027bdea9053a3abd95b", - "token_correspondence_PropImpredicativeAndNonStrictlyPositiveInductives.inj" - ], - 0, - "e09889f38c63080c01acfcce7321f324" - ], - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.f_injective", - 1, - 2, - 1, - [ - "@query", - "equation_PropImpredicativeAndNonStrictlyPositiveInductives.f", - "projection_inverse_PropImpredicativeAndNonStrictlyPositiveInductives.IntroA__0" - ], - 0, - "3a8105c7dce94c5b371061c451c33deb" - ], - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.p0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.l_Exists", - "equation_Prims.squash", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", - "unit_inversion" - ], - 0, - "49607f7b3c09cd6f131adf794c47967c" - ], - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.bad1", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "equation_PropImpredicativeAndNonStrictlyPositiveInductives.x0", - "function_token_typing_PropImpredicativeAndNonStrictlyPositiveInductives.p0", - "refinement_interpretation_Tm_refine_104aa28b549e0db1b9235eb785e4cc79" - ], - 0, - "2e93369deca1cbe83cfc0da2c5683cbb" - ], - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.bad2", - 1, - 2, - 1, - [ - "@query", - "equation_PropImpredicativeAndNonStrictlyPositiveInductives.p0", - "equation_PropImpredicativeAndNonStrictlyPositiveInductives.x0", - "function_token_typing_PropImpredicativeAndNonStrictlyPositiveInductives.p0", - "l_quant_interp_47acc1ba6e48f85f7ef66adc112f8bce" - ], - 0, - "1f73610f1e4362a25dc746477c31d245" - ], - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.bad", - 1, - 2, - 1, - [ "@query" ], - 0, - "1cd78121d3c054bacbd9a6b3988ee24e" - ], - [ - "PropImpredicativeAndNonStrictlyPositiveInductives.worse", - 1, - 2, - 1, - [ "@query" ], - 0, - "9116aceb3b4f7e895640df440f5f3cad" - ] - ] -] \ No newline at end of file diff --git a/examples/termination/maxime.fst.hints b/examples/termination/maxime.fst.hints deleted file mode 100644 index d5bf27e89d0..00000000000 --- a/examples/termination/maxime.fst.hints +++ /dev/null @@ -1 +0,0 @@ -[ "k\bP݈J=L\u0014m", [] ] \ No newline at end of file diff --git a/examples/termination/termination.fst.hints b/examples/termination/termination.fst.hints deleted file mode 100644 index 6cb4e7587cd..00000000000 --- a/examples/termination/termination.fst.hints +++ /dev/null @@ -1,438 +0,0 @@ -[ - "-ƐGU +#\u0007]F", - [ - [ - "Termination.factorial", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equation_Prims.nat", - "int_inversion", "int_typing", "primitive_Prims.op_Addition", - "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "well-founded-ordering-on-nat" - ], - 0, - "22420c3d0e9d7b45732ab58aff4c5259" - ], - [ - "Termination.fibonacci", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equation_Prims.nat", - "int_inversion", "int_typing", "primitive_Prims.op_Addition", - "primitive_Prims.op_LessThanOrEqual", - "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "well-founded-ordering-on-nat" - ], - 0, - "946ef0539d60197c5cbe027004e6a5a9" - ], - [ - "Termination.ackermann", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Prims_pretyping_ae567c2fb75be05905677af440075565", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "equation_Prims.nat", - "function_token_typing_Prims.__cache_version_number__", - "int_inversion", "int_typing", "primitive_Prims.op_Addition", - "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", - "projection_inverse_BoxBool_proj_0", - "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "well-founded-ordering-on-nat" - ], - 0, - "62e4dc7e0aa9011a56dfa8b49a858e3c" - ], - [ - "Termination.ack_swap", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Prims_pretyping_ae567c2fb75be05905677af440075565", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "equation_Prims.nat", - "function_token_typing_Prims.__cache_version_number__", - "int_inversion", "int_typing", "primitive_Prims.op_Addition", - "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", - "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "well-founded-ordering-on-nat" - ], - 0, - "936a0de9e95f036bda8349514dc8638d" - ], - [ - "Termination.length", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "equation_Prims.nat", "fuel_guarded_inversion_Prims.list", - "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", - "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "subterm_ordering_Prims.Cons" - ], - 0, - "a9b819daa9379685334b8ad8f842682d" - ], - [ - "Termination.half_length", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2", - "binder_x_fe28d8bcde588226b4e538b35321de05_1", - "constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons", - "disc_equation_Prims.Nil", "equation_Prims.nat", - "fuel_guarded_inversion_Prims.list", "primitive_Prims.op_Addition", - "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0", - "projection_inverse_BoxInt_proj_0", - "projection_inverse_Prims.Cons_a", - "projection_inverse_Prims.Cons_hd", - "projection_inverse_Prims.Cons_tl", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32", - "subterm_ordering_Prims.Cons", "typing_Prims.__proj__Cons__item__tl" - ], - 0, - "5ec199c12e33e1f7b6293ccb0e3916d3" - ], - [ - "Termination.sumto", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Prims_pretyping_ae567c2fb75be05905677af440075565", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equation_Prims.nat", - "function_token_typing_Prims.__cache_version_number__", - "int_inversion", "primitive_Prims.op_Addition", - "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", - "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "well-founded-ordering-on-nat" - ], - 0, - "7b3509399c77d64eba408fcd9a423162" - ], - [ - "Termination.strangeZero", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equation_Prims.nat", - "int_inversion", "primitive_Prims.op_Equality", - "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "well-founded-ordering-on-nat" - ], - 0, - "2e6558e66208d66e054554ca08a1bc21" - ], - [ - "Termination.map", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_3dddec8ced2db740e4e8aaf70542be7a_5", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "fuel_guarded_inversion_Prims.list", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" - ], - 0, - "c5fcd5c52ceefd84665e713f31058ab3" - ], - [ - "Termination.mem", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_374b44ccfcb77ed85d505dbc44265913_2", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "fuel_guarded_inversion_Prims.list", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" - ], - 0, - "35e3b64fc0827de51e617aa3d47416a9" - ], - [ - "Termination.list_subterm_ordering_coercion", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Termination.mem.fuel_instrumented", - "@fuel_irrelevance_Termination.mem.fuel_instrumented", "@query", - "binder_x_270b3cef5784d1bc5a7008b8b6b27eb6_3", - "binder_x_9cd1733a5204f989dbb2f01d5984df93_1", - "binder_x_b854bcaec29d9b05432d1478cbd54165_4", - "binder_x_fe28d8bcde588226b4e538b35321de05_2", "bool_inversion", - "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "equation_Prims.eqtype", "equation_Prims.op_Equals_Equals_Equals", - "equation_with_fuel_Termination.mem.fuel_instrumented", - "fuel_guarded_inversion_Prims.list", "primitive_Prims.op_BarBar", - "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", - "projection_inverse_Prims.Cons_a", - "projection_inverse_Prims.Cons_hd", - "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", - "refinement_interpretation_Tm_refine_7f65e6e96a286ef2fcef6eeaaf4a433e", - "refinement_interpretation_Tm_refine_8b5eece02e0724cd5f7835467ce93986", - "refinement_interpretation_Tm_refine_a0e30473eb82c18d4e4dc1a1cc3d49bf", - "refinement_interpretation_Tm_refine_fda41bc1aa39f7ec9fc4248687c58467", - "subterm_ordering_Prims.Cons", - "token_correspondence_Termination.mem.fuel_instrumented", - "typing_Termination.list_subterm_ordering_coercion", - "typing_Termination.mem" - ], - 0, - "d593947cbd3260e78715d825327be9b9" - ], - [ - "Termination.list_subterm_ordering_coercion", - 2, - 2, - 1, - [ "@query" ], - 0, - "7c726d211ba16fc028511da9834d4bd0" - ], - [ - "Termination.list_subterm_ordering_lemma", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Termination.mem.fuel_instrumented", - "@fuel_irrelevance_Termination.mem.fuel_instrumented", "@query", - "binder_x_270b3cef5784d1bc5a7008b8b6b27eb6_3", - "binder_x_9cd1733a5204f989dbb2f01d5984df93_1", - "binder_x_d3faed7bbec7b3b3d41ce73e2f001f5c_5", - "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "equation_with_fuel_Termination.mem.fuel_instrumented", - "fuel_guarded_inversion_Prims.list", "primitive_Prims.op_BarBar", - "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", - "projection_inverse_Prims.Cons_a", - "projection_inverse_Prims.Cons_hd", - "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", - "subterm_ordering_Prims.Cons" - ], - 0, - "330fa3c64e3117f2e350dc6bc0ba8e31" - ], - [ - "Termination.move_refinement", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Termination.mem.fuel_instrumented", - "@fuel_irrelevance_Termination.mem.fuel_instrumented", "@query", - "binder_x_9cd1733a5204f989dbb2f01d5984df93_0", - "binder_x_ee831b716a424052bd35b1d95526a186_2", - "constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons", - "disc_equation_Prims.Nil", - "equation_with_fuel_Termination.mem.fuel_instrumented", - "fuel_guarded_inversion_Prims.list", "primitive_Prims.op_BarBar", - "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", - "projection_inverse_Prims.Cons_a", - "projection_inverse_Prims.Cons_hd", - "projection_inverse_Prims.Cons_tl", - "refinement_interpretation_Tm_refine_52da1e478474dd908d45a896648a7fbc", - "subterm_ordering_Prims.Cons" - ], - 0, - "b8cec619b6cf329e13c596a789f8b487" - ], - [ - "Termination.tree", - 1, - 2, - 1, - [ - "@query", "assumption_Prims.list__uu___haseq", - "kinding_Termination.tree@tok" - ], - 0, - "904aa3a577d0c35761ce6ff6778dc1d1" - ], - [ - "Termination.__proj__Leaf__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_eecc20c444854ed8824621455f36b0bc" - ], - 0, - "8318e0309d5510bf222488b939ca14e1" - ], - [ - "Termination.__proj__Node__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_ef7437472d1ef108a142a5a0fa28c50f" - ], - 0, - "401820de9a40346e8579fe990dcde0c6" - ], - [ - "Termination.treeMap", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Termination.mem.fuel_instrumented", - "@fuel_irrelevance_Termination.mem.fuel_instrumented", "@query", - "assumption_Termination.tree__uu___haseq", - "binder_x_32126e64b1040b93adb289317bd0c1e7_4", - "binder_x_9cd1733a5204f989dbb2f01d5984df93_1", - "disc_equation_Termination.Leaf", "disc_equation_Termination.Node", - "equation_Prims.eqtype", "fuel_guarded_inversion_Termination.tree", - "kinding_Termination.tree@tok", - "lemma_Termination.list_subterm_ordering_lemma", - "projection_inverse_BoxBool_proj_0", - "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", - "subterm_ordering_Termination.Node" - ], - 0, - "0bb9d892c874c0c129cf7aec804b1911" - ], - [ - "Termination.list_map", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_3dddec8ced2db740e4e8aaf70542be7a_4", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "fuel_guarded_inversion_Prims.list", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" - ], - 0, - "7d5d9ff4e0d072d8558c36a8e393e226" - ], - [ - "Termination.tree_map", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_1b42b469d51f8d2af3c337b491db6005_5", - "disc_equation_Termination.Leaf", "disc_equation_Termination.Node", - "fuel_guarded_inversion_Termination.tree", - "projection_inverse_BoxBool_proj_0", - "subterm_ordering_Termination.Node" - ], - 0, - "3ea225d38dc11ff96aab42888025e5d9" - ], - [ - "Termination.flatten_list", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_8e2b3e2e2d5822bdb0266bcb517fa74a_4", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "fuel_guarded_inversion_Prims.list", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" - ], - 0, - "14cb36e52bc25250a9351002b0cc4116" - ], - [ - "Termination.flatten_tree", - 1, - 2, - 1, - [ - "@MaxFuel_assumption", "@MaxIFuel_assumption", - "@fuel_correspondence_Termination.mem.fuel_instrumented", - "@fuel_irrelevance_Termination.mem.fuel_instrumented", "@query", - "assumption_Termination.tree__uu___haseq", - "binder_x_484068bc8cf479ceebfc1c093bca5255_1", - "binder_x_9cd1733a5204f989dbb2f01d5984df93_0", - "disc_equation_Termination.Leaf", "disc_equation_Termination.Node", - "equation_Prims.eqtype", "fuel_guarded_inversion_Termination.tree", - "kinding_Termination.tree@tok", - "lemma_Termination.list_subterm_ordering_lemma", - "projection_inverse_BoxBool_proj_0", - "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", - "subterm_ordering_Termination.Node" - ], - 0, - "8aaa46d84e366779836dd0f1723af661" - ], - [ - "Termination.flatten_list'", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_8e2b3e2e2d5822bdb0266bcb517fa74a_4", - "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", - "fuel_guarded_inversion_Prims.list", - "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" - ], - 0, - "f02c713957f4da2fc13ffc56bb8abeab" - ], - [ - "Termination.flatten_tree'", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "binder_x_5d03a1de8ce9244d969fb5b9e35a1b72_2", - "disc_equation_Termination.Leaf", "disc_equation_Termination.Node", - "fuel_guarded_inversion_Termination.tree", - "projection_inverse_BoxBool_proj_0", - "subterm_ordering_Termination.Node" - ], - 0, - "056b3bab77d4ecee7931a57492606833" - ] - ] -] \ No newline at end of file diff --git a/ulib/.hints/FStar.All.fst.hints b/ulib/.hints/FStar.All.fst.hints deleted file mode 100644 index e2f1f0582a8..00000000000 --- a/ulib/.hints/FStar.All.fst.hints +++ /dev/null @@ -1,17 +0,0 @@ -[ - "9\u000ew&w", - [ - [ - "FStar.All.__proj__Failure__item__uu___", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_149c6719f34c408becdf9120a4ae2d59" - ], - 0, - "6954d194c5c87447fe449b9ca66c67d9" - ] - ] -] \ No newline at end of file diff --git a/ulib/.hints/FStar.BaseTypes.fsti.hints b/ulib/.hints/FStar.BaseTypes.fsti.hints deleted file mode 100644 index e85d97fd03d..00000000000 --- a/ulib/.hints/FStar.BaseTypes.fsti.hints +++ /dev/null @@ -1 +0,0 @@ -[ "\u0006JS&JmEfs/", [] ] \ No newline at end of file diff --git a/ulib/.hints/FStar.IO.fst.hints b/ulib/.hints/FStar.IO.fst.hints deleted file mode 100644 index 69bf62514e6..00000000000 --- a/ulib/.hints/FStar.IO.fst.hints +++ /dev/null @@ -1 +0,0 @@ -[ "n@\u0011f\u0000J,oR", [] ] \ No newline at end of file diff --git a/ulib/.hints/FStar.Reflection.V1.Builtins.fsti.hints b/ulib/.hints/FStar.Reflection.V1.Builtins.fsti.hints deleted file mode 100644 index 02227779472..00000000000 --- a/ulib/.hints/FStar.Reflection.V1.Builtins.fsti.hints +++ /dev/null @@ -1 +0,0 @@ -[ "%)dG=\u0015B", [] ] \ No newline at end of file diff --git a/ulib/.hints/FStar.Reflection.V1.Data.fsti.hints b/ulib/.hints/FStar.Reflection.V1.Data.fsti.hints deleted file mode 100644 index 19488f951ae..00000000000 --- a/ulib/.hints/FStar.Reflection.V1.Data.fsti.hints +++ /dev/null @@ -1,955 +0,0 @@ -[ - "D)&\u000fU>q", - [ - [ - "FStar.Reflection.V1.Data.__proj__C_Int__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5faa3d085d6529796186d2f166ec3e3b" - ], - 0, - "484679cc5dbe3fbfe4b7c8f6ed526591" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_String__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_20333e6843d20bb61911371ec2d163f9" - ], - 0, - "0b3f933584ec2dbeb16a5467b1388209" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Range__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_b5d9cb8b96e7aa7e89d03554e19f54d1" - ], - 0, - "071b8cbda52752d3f19e1915b9216829" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Reflect__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_af549649e5c395212daa7d7972b2fa6c" - ], - 0, - "8b8539b73c75c721e4e9b3e6d086ecf3" - ], - [ - "FStar.Reflection.V1.Data.__proj__Pat_Constant__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_9d623f63121aabf00b7a6c2ed62a1c39" - ], - 0, - "4f14156658cf2b3204c458981d4b4731" - ], - [ - "FStar.Reflection.V1.Data.__proj__Pat_Cons__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_d37fd99d741f59e6859367a7115261d5" - ], - 0, - "934ff472dbc82e96bcf298a95010bee9" - ], - [ - "FStar.Reflection.V1.Data.__proj__Pat_Cons__item___1", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_d37fd99d741f59e6859367a7115261d5" - ], - 0, - "4f5823f142f3ff5e2756cc82af50eca0" - ], - [ - "FStar.Reflection.V1.Data.__proj__Pat_Cons__item___2", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_d37fd99d741f59e6859367a7115261d5" - ], - 0, - "de79267dbc102b5622a8105f0f69562a" - ], - [ - "FStar.Reflection.V1.Data.__proj__Pat_Var__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_b054274b17dabddd2297af2c70372aa5" - ], - 0, - "c52659f35d3f6d441392b69cab63e92f" - ], - [ - "FStar.Reflection.V1.Data.__proj__Pat_Var__item___1", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_b054274b17dabddd2297af2c70372aa5" - ], - 0, - "32b34010a9bcf411f5f6e554d2ec66ca" - ], - [ - "FStar.Reflection.V1.Data.__proj__Pat_Dot_Term__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_32857d2ae27267a29cf8705f99948fe4" - ], - 0, - "b80372c77a6db155e398cc8fb64d72a9" - ], - [ - "FStar.Reflection.V1.Data.__proj__Q_Meta__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0c0becfe1087eb1a2e96cfe0e3f84488" - ], - 0, - "e5cff0bc27d59f626e124e0e344a6b01" - ], - [ - "FStar.Reflection.V1.Data.__proj__Uv_Succ__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_f469f8548f3b6e6c539e4a528c5a13fd" - ], - 0, - "0a7749c852a29ddefd74e2d8bc25c6b7" - ], - [ - "FStar.Reflection.V1.Data.__proj__Uv_Max__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_673ba89f3ec96045465ef1c7bc1da526" - ], - 0, - "cfa208d21bd0a0c0351d16121ffe8667" - ], - [ - "FStar.Reflection.V1.Data.__proj__Uv_BVar__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0bccbb9d82a71b03568292ca3b6e2e2c" - ], - 0, - "4a33d51f816899cf43abacbb71b5654d" - ], - [ - "FStar.Reflection.V1.Data.__proj__Uv_Name__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_cfa6fd28fe814f8756341be41995bc20" - ], - 0, - "b505154796f432e1537d198f3fb57450" - ], - [ - "FStar.Reflection.V1.Data.__proj__Uv_Unif__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_34e35b938cb965c3284c46d46fda950c" - ], - 0, - "07566fe7e0f3caa93a54dda4a92b163d" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Var__item__v", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_ac7ab67a82b9d6a7f0756b15a2d8dbd9" - ], - 0, - "f94430407c10d0d4c36efcabf9b3233b" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_BVar__item__v", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_f436b7d3d2f02c9267c5aabde2b87606" - ], - 0, - "d24f3992e906622e19b4806a3e5e2673" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_FVar__item__v", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_f11656ac8d25912e4fb3284f32b71abd" - ], - 0, - "02a021c451b52d72cc83403568fcb8ff" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_UInst__item__v", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5acf95e7de71a6bcfb3b7a25dc7e50b3" - ], - 0, - "c856f4688a214e355be849e7f3750d15" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_UInst__item__us", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5acf95e7de71a6bcfb3b7a25dc7e50b3" - ], - 0, - "c7d7543a6b3555e8b03e9c3213b7323c" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_App__item__hd", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_563dd6c46b41527fa4608b62210fd6da" - ], - 0, - "d2c95520c07b880ce1903c04e8add531" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_App__item__a", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_563dd6c46b41527fa4608b62210fd6da" - ], - 0, - "3457f03e79f592e5258df62ebe7e5eea" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Abs__item__bv", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_8c42fe35f460045606da623e72254641" - ], - 0, - "3cf5646253bbbc1920f0b993c8c9127c" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Abs__item__body", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_8c42fe35f460045606da623e72254641" - ], - 0, - "4f24e62ed512b422e5261db2ef928f04" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Arrow__item__bv", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5730fe8e56c39c65a07a73afc6ec4cda" - ], - 0, - "2b2a394922fe33e359f2d2abeb6b3a44" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Arrow__item__c", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5730fe8e56c39c65a07a73afc6ec4cda" - ], - 0, - "8691d7ab6b365b066ac48769deafcd4f" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Type__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_af4274e7d4358b25287142e54dd2febd" - ], - 0, - "d6338003b1ed5c632dd42fde46d8500f" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Refine__item__bv", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5ff4de323a387a73a7ab910fc7e00ae7" - ], - 0, - "c648a51b046027b9a42e89bb77b7758a" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Refine__item__sort", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5ff4de323a387a73a7ab910fc7e00ae7" - ], - 0, - "77d7af8a68b896ee610a04aaa681bf31" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Refine__item__ref", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5ff4de323a387a73a7ab910fc7e00ae7" - ], - 0, - "67c6c9db6db4cf470b5daf5144a05b27" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Const__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_ab36f2c5a1987a868713af0740020802" - ], - 0, - "3aaa06925094ffe4c41ab4867460413c" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Uvar__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_26389b868214dcf3205bbfb6d6a82044" - ], - 0, - "180d09e57b4fc2a8740fb0cc6582437b" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Uvar__item___1", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_26389b868214dcf3205bbfb6d6a82044" - ], - 0, - "eafc4cfadf97495fb8d325c3e6e8ad6f" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Let__item__recf", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3aa3214956e95ba92710251de6ae8eee" - ], - 0, - "89b34bdb66cb6b5b8d841979f657f168" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Let__item__attrs", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3aa3214956e95ba92710251de6ae8eee" - ], - 0, - "ae84414ce34dde2b25c5da960817ad48" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Let__item__bv", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3aa3214956e95ba92710251de6ae8eee" - ], - 0, - "957f32a25ad0cd26a788a8532b710399" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Let__item__ty", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3aa3214956e95ba92710251de6ae8eee" - ], - 0, - "9462891d96ec16cb871902d4c20bdf7c" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Let__item__def", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3aa3214956e95ba92710251de6ae8eee" - ], - 0, - "0eb74a84aac100d67d1a7661d2ee923d" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Let__item__body", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_3aa3214956e95ba92710251de6ae8eee" - ], - 0, - "59630cf83e19f5b1b8b53db25f6bb848" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Match__item__scrutinee", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_763a4b5b6214e1dd87a03c65beb109e1" - ], - 0, - "e3d32a857ee4420607da9a6b54fa504c" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Match__item__ret", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_763a4b5b6214e1dd87a03c65beb109e1" - ], - 0, - "d2f553d51419de106d7fcc33ff581416" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_Match__item__brs", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_763a4b5b6214e1dd87a03c65beb109e1" - ], - 0, - "4ee6b7dc9aadad2596cb0bfb41576282" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedT__item__e", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0e4e467f2e7420d0a00c571d1b9f3c98" - ], - 0, - "d325680c7099b8934e09af4876f15cab" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedT__item__t", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0e4e467f2e7420d0a00c571d1b9f3c98" - ], - 0, - "ce1cba0cd2912a951de602b7972c1d08" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedT__item__tac", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0e4e467f2e7420d0a00c571d1b9f3c98" - ], - 0, - "de98d27b540e6acbc0f1e5bedc27e72b" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedT__item__use_eq", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0e4e467f2e7420d0a00c571d1b9f3c98" - ], - 0, - "df2a16c9a5b93f4d7fb6228e5a5ce51d" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedC__item__e", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_c70e5cc7fa76b0c5fafcadb1c6760f00" - ], - 0, - "538a14490b491d3e92cd1c4406d76b0a" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedC__item__c", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_c70e5cc7fa76b0c5fafcadb1c6760f00" - ], - 0, - "e399932ae57f672404807ac323beed19" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedC__item__tac", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_c70e5cc7fa76b0c5fafcadb1c6760f00" - ], - 0, - "fc3082b15b5f899fab2dead32b3e7b3c" - ], - [ - "FStar.Reflection.V1.Data.__proj__Tv_AscribedC__item__use_eq", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_c70e5cc7fa76b0c5fafcadb1c6760f00" - ], - 0, - "78a874042d40159b7609004da9ca53dd" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Total__item__ret", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_1da80b8d10b61c766ff8e467df7dd950" - ], - 0, - "fb42a87b9107f20c6b9e14ed11d4cd64" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_GTotal__item__ret", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0620da020c821ec7e521a018dce18ac1" - ], - 0, - "39bb836af285c7c26bdb5e13dfff5e96" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Lemma__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_e86623164f60a62649ddc84727261986" - ], - 0, - "5f736e1de185e27fffc68a664787d937" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Lemma__item___1", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_e86623164f60a62649ddc84727261986" - ], - 0, - "61752a1a8405bac9aef1d911073be15f" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Lemma__item___2", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_e86623164f60a62649ddc84727261986" - ], - 0, - "66d0801c274fed99f5443b4d450bc46f" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Eff__item__us", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a1a95e70a5bb3bd58904b1f905f8f614" - ], - 0, - "7153200c1143ec93c7fad7b9fb2ddd1d" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Eff__item__eff_name", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a1a95e70a5bb3bd58904b1f905f8f614" - ], - 0, - "482b758632c84051ec28508c613d08bb" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Eff__item__result", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a1a95e70a5bb3bd58904b1f905f8f614" - ], - 0, - "65b41e8f276681ea366fe54dce075a10" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Eff__item__eff_args", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a1a95e70a5bb3bd58904b1f905f8f614" - ], - 0, - "8d6a5b5c06d554616f904666a3b0bcd9" - ], - [ - "FStar.Reflection.V1.Data.__proj__C_Eff__item__decrs", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a1a95e70a5bb3bd58904b1f905f8f614" - ], - 0, - "e796740b48838bf22581c8fba5250652" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Let__item__r", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_6823610c6506c42a7079b513145ff476" - ], - 0, - "eea1a3f9080bcd2056dc8ffd8839ee92" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Let__item__lbs", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_6823610c6506c42a7079b513145ff476" - ], - 0, - "a34f71ca84a8bd7bb909abc68e030f7b" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Inductive__item__nm", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_53eda7b16bf0d76ac6387bfe75b9c989" - ], - 0, - "56022811a803cb161b43c02575bd6c00" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Inductive__item__univs", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_53eda7b16bf0d76ac6387bfe75b9c989" - ], - 0, - "1ffa34f90ab24a1057d95f2b7a8533a4" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Inductive__item__params", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_53eda7b16bf0d76ac6387bfe75b9c989" - ], - 0, - "361c2f536cbddc0721b74dd97020d51e" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Inductive__item__typ", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_53eda7b16bf0d76ac6387bfe75b9c989" - ], - 0, - "a2814f7fb000b50a6da940fe987cfdeb" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Inductive__item__cts", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_53eda7b16bf0d76ac6387bfe75b9c989" - ], - 0, - "1d48d606b2941d17d92189ccc60be0ea" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Val__item__nm", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_499901c8bdeb6207051525350960057b" - ], - 0, - "62ed52f6b4f8dc3385ca56274c6d070c" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Val__item__univs", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_499901c8bdeb6207051525350960057b" - ], - 0, - "4df01ffffe0824c41aa69c91d8ea671a" - ], - [ - "FStar.Reflection.V1.Data.__proj__Sg_Val__item__typ", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_499901c8bdeb6207051525350960057b" - ], - 0, - "d70fe69a3738122910adcf1e260b0a22" - ], - [ - "FStar.Reflection.V1.Data.__proj__Reflectable__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_c598b0fcb6018215b34a0a0f4175ab3f" - ], - 0, - "3220ce1156d28958f12905d1077d8321" - ], - [ - "FStar.Reflection.V1.Data.__proj__Discriminator__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_f97eda6eaf064cc6a32252c6aeb9db00" - ], - 0, - "45f82e7e7e4e08c07098d92c962a91e0" - ], - [ - "FStar.Reflection.V1.Data.__proj__Projector__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0cb9146dcf278ad296f8fcd7574c46e6" - ], - 0, - "c203005712da30c756b2b7fc33a254ad" - ], - [ - "FStar.Reflection.V1.Data.__proj__RecordType__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a4eb03973cc92f16348ebfcc38b2ccf6" - ], - 0, - "b0aa3d77abe0cc5d3b2fff1b4ff884b9" - ], - [ - "FStar.Reflection.V1.Data.__proj__RecordConstructor__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_56d2fc442b33085f467ecf131b1ccb32" - ], - 0, - "8b22c7f046515a2b863d82699df3e87e" - ], - [ - "FStar.Reflection.V1.Data.__proj__Action__item___0", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_5e24d81c8869a32e4083ec2aedc05d68" - ], - 0, - "f3894aa9e7bcaef6e376f7e96814497f" - ], - [ - "FStar.Reflection.V1.Data.var", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", - "equation_Prims.nat", "function_token_typing_Prims.int", - "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", - "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" - ], - 0, - "14fd60352843d723d0f18a128b6423e5" - ] - ] -] \ No newline at end of file diff --git a/ulib/.hints/FStar.Reflection.V2.Builtins.fsti.hints b/ulib/.hints/FStar.Reflection.V2.Builtins.fsti.hints deleted file mode 100644 index 7ab386a9453..00000000000 --- a/ulib/.hints/FStar.Reflection.V2.Builtins.fsti.hints +++ /dev/null @@ -1 +0,0 @@ -[ "4N\bٷ\u007f˿2ַ", [] ] \ No newline at end of file diff --git a/ulib/.hints/FStar.Reflection.V2.Data.fsti.hints b/ulib/.hints/FStar.Reflection.V2.Data.fsti.hints deleted file mode 100644 index 10ac764cb0b..00000000000 --- a/ulib/.hints/FStar.Reflection.V2.Data.fsti.hints +++ /dev/null @@ -1,931 +0,0 @@ -[ - "A#:Hhֵ\u0011", [] ] \ No newline at end of file diff --git a/ulib/.hints/FStar.Tactics.fst.hints b/ulib/.hints/FStar.Tactics.fst.hints deleted file mode 100644 index f5f50c51779..00000000000 --- a/ulib/.hints/FStar.Tactics.fst.hints +++ /dev/null @@ -1 +0,0 @@ -[ "\u001e\u0014#\u0013&Xm\u001a", [] ] \ No newline at end of file diff --git a/ulib/.hints/FStar.VConfig.fsti.hints b/ulib/.hints/FStar.VConfig.fsti.hints deleted file mode 100644 index fd101ccbf19..00000000000 --- a/ulib/.hints/FStar.VConfig.fsti.hints +++ /dev/null @@ -1,21 +0,0 @@ -[ - "_-:Nu\u0004aN", - [ - [ - "FStar.VConfig.vconfig", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Prims_pretyping_ce036b6b736ef4e0bc3a9ff132a12aed", - "assumption_FStar.Pervasives.Native.option__uu___haseq", - "assumption_Prims.list__uu___haseq", "equation_Prims.eqtype", - "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", - "typing_Prims.string" - ], - 0, - "6f5d61ba6d621a38e60753eef0f746da" - ] - ] -] \ No newline at end of file