mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-20 00:41:05 +03:00
1659 lines
77 KiB
Plaintext
1659 lines
77 KiB
Plaintext
[
|
||
"ÈRZ<\u0003\u001a\u0014]\u001bàós˜<73>\u001a ",
|
||
[
|
||
[
|
||
"Catala.DefaultCalculus.ty",
|
||
1,
|
||
2,
|
||
1,
|
||
[ "@query" ],
|
||
0,
|
||
"12150cad5f4ddd027a123d3c1158bd22"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__TArrow__item__tin",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee"
|
||
],
|
||
0,
|
||
"f5a4a5e56629567a3f3abebc47a175f6"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__TArrow__item__tout",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee"
|
||
],
|
||
0,
|
||
"32aa6b12103fab987cab73d2805b8c4c"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.exp",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"assumption_Catala.DefaultCalculus.lit__uu___haseq",
|
||
"assumption_Catala.DefaultCalculus.ty__uu___haseq",
|
||
"assumption_Prims.list__uu___haseq",
|
||
"equation_Catala.DefaultCalculus.var", "equation_Prims.eqtype",
|
||
"equation_Prims.nat", "function_token_typing_Prims.int",
|
||
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"kinding_Catala.DefaultCalculus.exp@tok",
|
||
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
|
||
],
|
||
0,
|
||
"5c21ef04a7f1a272f0a758c0f9d4157f"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EVar__item__v",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_f7bcdc7958786fcb60dfc7f410094686"
|
||
],
|
||
0,
|
||
"86d09cadd40705978f79fb65229cc940"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EApp__item__fn",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||
],
|
||
0,
|
||
"f936cabcaa864c9de9ef7060d4beda9e"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EApp__item__arg",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||
],
|
||
0,
|
||
"9a2c69a981e794b9f0b928d48bf90ae3"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EApp__item__tau_arg",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||
],
|
||
0,
|
||
"ab25b3f78be3cc5aabd9f1fd351a0bc1"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EAbs__item__vty",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5"
|
||
],
|
||
0,
|
||
"74f08bfcc019ccad07bdf4b110444b3e"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EAbs__item__body",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5"
|
||
],
|
||
0,
|
||
"a8f6ac1b8b1eadf6a785be3fe9fb927a"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__ELit__item__l",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_6ccee90986879ff2274b72e5bc3434cf"
|
||
],
|
||
0,
|
||
"ff76bf58b2a6d5314cdde4b538aba56c"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EIf__item__test",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||
],
|
||
0,
|
||
"cd48dc9eb173c293455593df0f6845f8"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EIf__item__btrue",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||
],
|
||
0,
|
||
"64ea55616f7ddf6ca1e471e4aaff7d9b"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EIf__item__bfalse",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||
],
|
||
0,
|
||
"cd4749573d6077d9736cda47882cdfee"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__exceptions",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"cf49a90661edd3f0858eb2722af413f4"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__just",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"c9df05fe32fbcde1f09ce17d029667ea"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__cons",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"93ff28a22eb5be2147e7adea388d6cfd"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__tau",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"ae54db2c6ac7a040b9bb50d0307b53ec"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.is_renaming_prop",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"equation_Catala.DefaultCalculus.var", "equation_Prims.l_Forall",
|
||
"equation_Prims.nat", "equation_Prims.squash",
|
||
"equation_Prims.subtype_of",
|
||
"l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
|
||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||
],
|
||
0,
|
||
"a5871f23ea914484dbc8d47a28d16241"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.is_renaming_size",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1c1d1c6e28a4d07ae30d44381ee0d524"
|
||
],
|
||
0,
|
||
"0d5c9fb7f30a119d4b46e222cefd114a"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.increment",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"equation_Catala.DefaultCalculus.var", "equation_Prims.nat",
|
||
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||
],
|
||
0,
|
||
"4ee76b70ce018b172689339c1f9ba1a7"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.increment_is_renaming",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@query", "constructor_distinct_Catala.DefaultCalculus.EVar",
|
||
"disc_equation_Catala.DefaultCalculus.EVar",
|
||
"equation_Catala.DefaultCalculus.increment",
|
||
"equation_Catala.DefaultCalculus.is_renaming_prop",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EVar_v"
|
||
],
|
||
0,
|
||
"6e078d9ccf128e72e747d681859fec07"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.subst",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_16e47229fa4f513e4aff966f842aa522",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_e31a3c19683e8b2fd2b67c21ce8e4ced",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_1",
|
||
"binder_x_6c50c515b77925886e3faaa30943f0fb_0", "bool_inversion",
|
||
"constructor_distinct_Catala.DefaultCalculus.EAbs",
|
||
"constructor_distinct_Catala.DefaultCalculus.EApp",
|
||
"constructor_distinct_Catala.DefaultCalculus.EIf",
|
||
"constructor_distinct_Catala.DefaultCalculus.ELit",
|
||
"constructor_distinct_Catala.DefaultCalculus.EVar",
|
||
"data_elim_Catala.DefaultCalculus.EVar",
|
||
"disc_equation_Catala.DefaultCalculus.EAbs",
|
||
"disc_equation_Catala.DefaultCalculus.EApp",
|
||
"disc_equation_Catala.DefaultCalculus.EDefault",
|
||
"disc_equation_Catala.DefaultCalculus.EIf",
|
||
"disc_equation_Catala.DefaultCalculus.ELit",
|
||
"disc_equation_Catala.DefaultCalculus.EVar",
|
||
"equation_Catala.DefaultCalculus.is_renaming_prop",
|
||
"equation_Catala.DefaultCalculus.is_renaming_size",
|
||
"equation_Catala.DefaultCalculus.is_var_size",
|
||
"equation_Catala.DefaultCalculus.var",
|
||
"equation_Catala.DefaultCalculus.var_to_exp", "equation_Prims.nat",
|
||
"equation_Prims.prop",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"function_token_typing_Catala.DefaultCalculus.subst_abs",
|
||
"function_token_typing_Prims.__cache_version_number__",
|
||
"int_inversion", "int_typing", "projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EAbs_body",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_fn",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_bfalse",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_btrue",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_test",
|
||
"projection_inverse_Catala.DefaultCalculus.EVar_v",
|
||
"refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"refinement_interpretation_Tm_refine_73f210ca6e0061ed4a3150f69b8f33bf",
|
||
"refinement_interpretation_Tm_refine_796ea366a949e0b57c08263b6d4daad3",
|
||
"refinement_interpretation_Tm_refine_829234be963617554f5a7b8433c93f5c",
|
||
"refinement_interpretation_Tm_refine_bcced13304791c2e1ef0eb3c0488e66c",
|
||
"subterm_ordering_Catala.DefaultCalculus.EAbs",
|
||
"subterm_ordering_Catala.DefaultCalculus.EApp",
|
||
"subterm_ordering_Catala.DefaultCalculus.EDefault",
|
||
"subterm_ordering_Catala.DefaultCalculus.EIf",
|
||
"token_correspondence_Catala.DefaultCalculus.subst_abs",
|
||
"typing_Catala.DefaultCalculus.is_renaming_prop",
|
||
"typing_Catala.DefaultCalculus.is_renaming_size",
|
||
"typing_Catala.DefaultCalculus.is_var_size",
|
||
"typing_Catala.DefaultCalculus.uu___is_EVar",
|
||
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
|
||
"well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"2ac81019ed65010c01639cde5ce4bd24"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.subst",
|
||
2,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_374a7fe1e57403f158e71980a97ecb0e_1",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"equation_Catala.DefaultCalculus.is_var_size",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"function_token_typing_Prims.__cache_version_number__", "int_typing",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons",
|
||
"typing_Catala.DefaultCalculus.is_var_size",
|
||
"well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"0d5ade8a32c11b981665f8671b91057a"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.subst",
|
||
3,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_6c50c515b77925886e3faaa30943f0fb_0",
|
||
"binder_x_c7c057bcb1ada4a7fe94b1a061987144_1", "bool_inversion",
|
||
"constructor_distinct_Catala.DefaultCalculus.EVar",
|
||
"disc_equation_Catala.DefaultCalculus.EVar",
|
||
"equation_Catala.DefaultCalculus.increment",
|
||
"equation_Catala.DefaultCalculus.is_renaming_prop",
|
||
"equation_Catala.DefaultCalculus.is_renaming_size",
|
||
"equation_Catala.DefaultCalculus.is_var_size",
|
||
"equation_Catala.DefaultCalculus.var", "equation_Prims.nat",
|
||
"equation_Prims.prop",
|
||
"function_token_typing_Prims.__cache_version_number__",
|
||
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
|
||
"primitive_Prims.op_Subtraction",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EVar_v",
|
||
"refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"refinement_interpretation_Tm_refine_73f210ca6e0061ed4a3150f69b8f33bf",
|
||
"refinement_interpretation_Tm_refine_796ea366a949e0b57c08263b6d4daad3",
|
||
"typing_Catala.DefaultCalculus.increment",
|
||
"typing_Catala.DefaultCalculus.is_renaming_prop",
|
||
"typing_Catala.DefaultCalculus.is_renaming_size",
|
||
"typing_Catala.DefaultCalculus.is_var_size",
|
||
"typing_Catala.DefaultCalculus.uu___is_EVar",
|
||
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
|
||
"well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"91b895d6b22c636592ada525fa8b6e21"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.var_to_exp_beta",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"equation_Catala.DefaultCalculus.var", "equation_Prims.nat",
|
||
"int_inversion", "primitive_Prims.op_Equality",
|
||
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||
],
|
||
0,
|
||
"4919dd145a17c7faf0fa0134990f7e24"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.empty_count_result",
|
||
1,
|
||
2,
|
||
1,
|
||
[ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ],
|
||
0,
|
||
"05a61ea6afa54b936185f89ab9f81057"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__OneNonEmpty__item___0",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_73db3433a5536656aa27657eb477efcf"
|
||
],
|
||
0,
|
||
"4c9e376e3b1d380a9a228dc4cde9412d"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.exceptions_count_result",
|
||
1,
|
||
2,
|
||
1,
|
||
[ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ],
|
||
0,
|
||
"5b75d806bc2195f123968f463592e8c7"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__SomeStep__item___0",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_562b75d472a96c36a24c70375d81f26c"
|
||
],
|
||
0,
|
||
"177794c807654230fd0f2a3c1064cb12"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.empty_count",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Catala.DefaultCalculus_pretyping_ddbfacc376d73d0ca810e3fd46e827d6",
|
||
"binder_x_374a7fe1e57403f158e71980a97ecb0e_1",
|
||
"binder_x_ddbfacc376d73d0ca810e3fd46e827d6_0",
|
||
"data_typing_intro_Catala.DefaultCalculus.Conflict@tok",
|
||
"disc_equation_Catala.DefaultCalculus.AllEmpty",
|
||
"disc_equation_Catala.DefaultCalculus.Conflict",
|
||
"disc_equation_Catala.DefaultCalculus.OneNonEmpty",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.empty_count_result",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
|
||
"subterm_ordering_Prims.Cons"
|
||
],
|
||
0,
|
||
"33fab59152a25fb11ae6416f0c1d7ffa"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.step_app",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"disc_equation_FStar.Pervasives.Native.None",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"kinding_Catala.DefaultCalculus.exp@tok",
|
||
"lemma_FStar.Pervasives.invertOption"
|
||
],
|
||
0,
|
||
"a7c323cfaba27d5e7df545707c3ca4ed"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.step_app",
|
||
2,
|
||
2,
|
||
1,
|
||
[
|
||
"@query", "kinding_Catala.DefaultCalculus.exp@tok",
|
||
"lemma_FStar.Pervasives.invertOption"
|
||
],
|
||
0,
|
||
"c09544ba3d4ab4c6a612329534698084"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.step_app",
|
||
3,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"binder_x_57403813bce408351cc0e70737e314ef_1",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_Prims.Cons_hd",
|
||
"projection_inverse_Prims.Cons_tl",
|
||
"refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1",
|
||
"subterm_ordering_Prims.Cons"
|
||
],
|
||
0,
|
||
"74d07d02a774893a2736842e43273b3f"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.step_app",
|
||
4,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.empty_count.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"binder_x_57403813bce408351cc0e70737e314ef_1",
|
||
"constructor_distinct_Catala.DefaultCalculus.AllEmpty",
|
||
"disc_equation_Catala.DefaultCalculus.AllEmpty",
|
||
"disc_equation_Catala.DefaultCalculus.Conflict",
|
||
"disc_equation_Catala.DefaultCalculus.OneNonEmpty",
|
||
"equality_tok_Catala.DefaultCalculus.AllEmpty@tok",
|
||
"equation_with_fuel_Catala.DefaultCalculus.empty_count.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.empty_count_result",
|
||
"function_token_typing_Prims.__cache_version_number__", "int_typing",
|
||
"kinding_Catala.DefaultCalculus.exp@tok",
|
||
"lemma_FStar.Pervasives.invertOption",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1",
|
||
"typing_Catala.DefaultCalculus.empty_count",
|
||
"typing_tok_Catala.DefaultCalculus.AllEmpty@tok",
|
||
"well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"85964bd5932ba9afbd2878998276dcb3"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.step_app",
|
||
5,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"disc_equation_Catala.DefaultCalculus.IllFormed",
|
||
"disc_equation_Catala.DefaultCalculus.NoStep",
|
||
"disc_equation_Catala.DefaultCalculus.SomeStep",
|
||
"disc_equation_FStar.Pervasives.Native.None",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exceptions_count_result",
|
||
"function_token_typing_Prims.__cache_version_number__", "int_typing",
|
||
"kinding_Catala.DefaultCalculus.exp@tok",
|
||
"lemma_FStar.Pervasives.invertOption",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"6720e36dd54fb92ae3cf738f1b6d99c7"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.step_app",
|
||
6,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"function_token_typing_Prims.__cache_version_number__", "int_typing",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"subterm_ordering_Catala.DefaultCalculus.EApp",
|
||
"subterm_ordering_Catala.DefaultCalculus.EDefault",
|
||
"subterm_ordering_Catala.DefaultCalculus.EIf",
|
||
"well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"48361c5e0ee8cdfa9389b377a1e1034e"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.extend",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"equation_Catala.DefaultCalculus.var", "equation_Prims.nat",
|
||
"int_inversion", "primitive_Prims.op_Equality",
|
||
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||
],
|
||
0,
|
||
"959e0ad7f119bf608ef98c6b407085a9"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.typing",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"assumption_Catala.DefaultCalculus.ty__uu___haseq",
|
||
"assumption_FStar.Pervasives.Native.option__uu___haseq",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_1",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"kinding_Catala.DefaultCalculus.ty@tok",
|
||
"subterm_ordering_Catala.DefaultCalculus.EAbs",
|
||
"subterm_ordering_Catala.DefaultCalculus.EApp",
|
||
"subterm_ordering_Catala.DefaultCalculus.EDefault",
|
||
"subterm_ordering_Catala.DefaultCalculus.EIf"
|
||
],
|
||
0,
|
||
"c00bf7a3d4293b2ca0d3f471a94a7443"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.typing",
|
||
2,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"binder_x_374a7fe1e57403f158e71980a97ecb0e_1",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons"
|
||
],
|
||
0,
|
||
"a912ce2537d5bd5b8efac5742694d5e0"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.is_bool_value_cannot_be_abs",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"bool_inversion",
|
||
"constructor_distinct_Catala.DefaultCalculus.TBool",
|
||
"constructor_distinct_Catala.DefaultCalculus.TUnit",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"equality_tok_Catala.DefaultCalculus.TBool@tok",
|
||
"equality_tok_Catala.DefaultCalculus.TUnit@tok",
|
||
"equation_Catala.DefaultCalculus.is_value",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
|
||
"typing_Catala.DefaultCalculus.is_value",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_tok_Catala.DefaultCalculus.TBool@tok"
|
||
],
|
||
0,
|
||
"fcce91fe26fc2f7278f943781c702e71"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.typing_conserved_by_list_reduction",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@query", "disc_equation_Prims.Cons",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"primitive_Prims.op_AmpAmp", "proj_equation_Prims.Cons_tl",
|
||
"projection_inverse_BoxBool_proj_0"
|
||
],
|
||
0,
|
||
"4cb4f790bd65800755bf9b124baf211b"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.progress",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step_default.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_default.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
|
||
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_1", "bool_inversion",
|
||
"constructor_distinct_Catala.DefaultCalculus.EApp",
|
||
"constructor_distinct_Catala.DefaultCalculus.EDefault",
|
||
"constructor_distinct_Catala.DefaultCalculus.EIf",
|
||
"constructor_distinct_Catala.DefaultCalculus.TArrow",
|
||
"constructor_distinct_Catala.DefaultCalculus.TBool",
|
||
"constructor_distinct_Catala.DefaultCalculus.TUnit",
|
||
"constructor_distinct_FStar.Pervasives.Native.None",
|
||
"constructor_distinct_FStar.Pervasives.Native.Some",
|
||
"data_elim_Catala.DefaultCalculus.EVar",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"disc_equation_Catala.DefaultCalculus.EApp",
|
||
"disc_equation_Catala.DefaultCalculus.EDefault",
|
||
"disc_equation_Catala.DefaultCalculus.EIf",
|
||
"disc_equation_FStar.Pervasives.Native.None",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"equality_tok_Catala.DefaultCalculus.TBool@tok",
|
||
"equality_tok_Catala.DefaultCalculus.TUnit@tok",
|
||
"equation_Catala.DefaultCalculus.empty",
|
||
"equation_Catala.DefaultCalculus.is_value",
|
||
"equation_Catala.DefaultCalculus.var",
|
||
"equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_app.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_if.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"function_token_typing_Prims.__cache_version_number__", "int_typing",
|
||
"interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af",
|
||
"kinding_Catala.DefaultCalculus.exp@tok",
|
||
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
|
||
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
|
||
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_fn",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_tau_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_bfalse",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_btrue",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_test",
|
||
"refinement_interpretation_Tm_refine_1f79706984431459041a6f7851223328",
|
||
"refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084",
|
||
"refinement_interpretation_Tm_refine_bc236faac1238ac3ee32de7f5026c212",
|
||
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"subterm_ordering_Catala.DefaultCalculus.EApp",
|
||
"subterm_ordering_Catala.DefaultCalculus.EDefault",
|
||
"subterm_ordering_Catala.DefaultCalculus.EIf",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"typing_Catala.DefaultCalculus.empty",
|
||
"typing_Catala.DefaultCalculus.is_value",
|
||
"typing_Catala.DefaultCalculus.step",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af",
|
||
"typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion",
|
||
"unit_typing", "well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"4dbdda6ef73e359692b6571a7ac927de"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.progress",
|
||
2,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step_default.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step_exceptions.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_app.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_default.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_if.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_5401141756166ef64ba94940663272f3",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Catala.DefaultCalculus_pretyping_6228a1bba9fe5ca24a1c0a49c31d0d53",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
|
||
"FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250",
|
||
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"binder_x_57403813bce408351cc0e70737e314ef_1",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_4",
|
||
"binder_x_9d898a02527d03c282f289aa9ecae7fc_2",
|
||
"binder_x_9d898a02527d03c282f289aa9ecae7fc_3", "bool_inversion",
|
||
"constructor_distinct_Catala.DefaultCalculus.EDefault",
|
||
"constructor_distinct_Catala.DefaultCalculus.ELit",
|
||
"constructor_distinct_Catala.DefaultCalculus.IllFormed",
|
||
"constructor_distinct_Catala.DefaultCalculus.LConflictError",
|
||
"constructor_distinct_Catala.DefaultCalculus.LEmptyError",
|
||
"constructor_distinct_Catala.DefaultCalculus.LFalse",
|
||
"constructor_distinct_Catala.DefaultCalculus.LTrue",
|
||
"constructor_distinct_Catala.DefaultCalculus.NoStep",
|
||
"constructor_distinct_Catala.DefaultCalculus.SomeStep",
|
||
"constructor_distinct_FStar.Pervasives.Native.None",
|
||
"constructor_distinct_FStar.Pervasives.Native.Some",
|
||
"constructor_distinct_Tm_unit",
|
||
"data_elim_Catala.DefaultCalculus.ELit",
|
||
"data_elim_Catala.DefaultCalculus.EVar",
|
||
"data_typing_intro_Catala.DefaultCalculus.LConflictError@tok",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"disc_equation_Catala.DefaultCalculus.ELit",
|
||
"disc_equation_Catala.DefaultCalculus.IllFormed",
|
||
"disc_equation_Catala.DefaultCalculus.LConflictError",
|
||
"disc_equation_Catala.DefaultCalculus.LEmptyError",
|
||
"disc_equation_Catala.DefaultCalculus.LFalse",
|
||
"disc_equation_Catala.DefaultCalculus.LTrue",
|
||
"disc_equation_Catala.DefaultCalculus.NoStep",
|
||
"disc_equation_Catala.DefaultCalculus.SomeStep",
|
||
"disc_equation_FStar.Pervasives.Native.None",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"equality_tok_Catala.DefaultCalculus.IllFormed@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LConflictError@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LEmptyError@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LFalse@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LTrue@tok",
|
||
"equality_tok_Catala.DefaultCalculus.NoStep@tok",
|
||
"equality_tok_Catala.DefaultCalculus.TBool@tok",
|
||
"equation_Catala.DefaultCalculus.empty",
|
||
"equation_Catala.DefaultCalculus.is_value",
|
||
"equation_Catala.DefaultCalculus.var",
|
||
"equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_default.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_exceptions.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exceptions_count_result",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.lit",
|
||
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
|
||
"function_token_typing_Catala.DefaultCalculus.is_value",
|
||
"function_token_typing_Prims.__cache_version_number__",
|
||
"int_inversion", "int_typing",
|
||
"interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af",
|
||
"kinding_Catala.DefaultCalculus.exp@tok",
|
||
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
|
||
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
|
||
"primitive_Prims.op_Equality",
|
||
"proj_equation_Catala.DefaultCalculus.ELit_l",
|
||
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||
"projection_inverse_Catala.DefaultCalculus.ELit_l",
|
||
"projection_inverse_Catala.DefaultCalculus.SomeStep__0",
|
||
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
|
||
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
|
||
"projection_inverse_FStar.Pervasives.Native.Some_a",
|
||
"projection_inverse_FStar.Pervasives.Native.Some_v",
|
||
"refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be",
|
||
"refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14",
|
||
"refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1",
|
||
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"typing_Catala.DefaultCalculus.empty",
|
||
"typing_Catala.DefaultCalculus.step_default",
|
||
"typing_Catala.DefaultCalculus.step_exceptions",
|
||
"typing_Catala.DefaultCalculus.step_exceptions_left_to_right",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_FStar.List.Tot.Base.for_all",
|
||
"typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af",
|
||
"typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion",
|
||
"unit_typing", "well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"5b33ceef79d8a11910f5923459b91078"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.progress",
|
||
3,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_irrelevance_FStar.List.Tot.Base.for_all.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_5401141756166ef64ba94940663272f3",
|
||
"FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"binder_x_57403813bce408351cc0e70737e314ef_1",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_4",
|
||
"binder_x_9d898a02527d03c282f289aa9ecae7fc_2",
|
||
"binder_x_9d898a02527d03c282f289aa9ecae7fc_3", "bool_inversion",
|
||
"constructor_distinct_Catala.DefaultCalculus.EDefault",
|
||
"constructor_distinct_Catala.DefaultCalculus.LConflictError",
|
||
"constructor_distinct_FStar.Pervasives.Native.None",
|
||
"constructor_distinct_FStar.Pervasives.Native.Some",
|
||
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
|
||
"constructor_distinct_Tm_unit", "data_elim_Prims.Cons",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"equality_tok_Catala.DefaultCalculus.LConflictError@tok",
|
||
"equation_Catala.DefaultCalculus.c_err",
|
||
"equation_Catala.DefaultCalculus.empty",
|
||
"equation_Catala.DefaultCalculus.is_value",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"function_token_typing_Catala.DefaultCalculus.is_value",
|
||
"kinding_Catala.DefaultCalculus.exp@tok",
|
||
"primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||
"projection_inverse_FStar.Pervasives.Native.Some_v",
|
||
"projection_inverse_Prims.Cons_a",
|
||
"projection_inverse_Prims.Cons_hd",
|
||
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
|
||
"refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084",
|
||
"refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be",
|
||
"refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14",
|
||
"refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1",
|
||
"subterm_ordering_Prims.Cons",
|
||
"token_correspondence_Catala.DefaultCalculus.is_value",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"typing_Catala.DefaultCalculus.empty",
|
||
"typing_Catala.DefaultCalculus.step_exceptions_left_to_right",
|
||
"typing_Catala.DefaultCalculus.typing_list",
|
||
"typing_FStar.List.Tot.Base.for_all"
|
||
],
|
||
0,
|
||
"49410cf76d076b55772b0c9a4b2de111"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.empty_count_preserves_type",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.empty_count.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.empty_count.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_pretyping_ddbfacc376d73d0ca810e3fd46e827d6",
|
||
"binder_x_374a7fe1e57403f158e71980a97ecb0e_1",
|
||
"binder_x_5fb06af9e7383e6ae83424b64f7b9e82_2",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_3",
|
||
"binder_x_ddbfacc376d73d0ca810e3fd46e827d6_0", "bool_inversion",
|
||
"constructor_distinct_Catala.DefaultCalculus.AllEmpty",
|
||
"constructor_distinct_Catala.DefaultCalculus.Conflict",
|
||
"constructor_distinct_Catala.DefaultCalculus.ELit",
|
||
"constructor_distinct_Catala.DefaultCalculus.LEmptyError",
|
||
"constructor_distinct_Catala.DefaultCalculus.OneNonEmpty",
|
||
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
|
||
"constructor_distinct_Tm_unit",
|
||
"data_elim_Catala.DefaultCalculus.OneNonEmpty",
|
||
"data_typing_intro_Catala.DefaultCalculus.Conflict@tok",
|
||
"disc_equation_Catala.DefaultCalculus.AllEmpty",
|
||
"disc_equation_Catala.DefaultCalculus.Conflict",
|
||
"disc_equation_Catala.DefaultCalculus.ELit",
|
||
"disc_equation_Catala.DefaultCalculus.LEmptyError",
|
||
"disc_equation_Catala.DefaultCalculus.OneNonEmpty",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"equality_tok_Catala.DefaultCalculus.AllEmpty@tok",
|
||
"equality_tok_Catala.DefaultCalculus.Conflict@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LEmptyError@tok",
|
||
"equation_with_fuel_Catala.DefaultCalculus.empty_count.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.empty_count_result",
|
||
"primitive_Prims.op_AmpAmp",
|
||
"proj_equation_Catala.DefaultCalculus.ELit_l",
|
||
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
|
||
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.ELit_l",
|
||
"projection_inverse_Catala.DefaultCalculus.OneNonEmpty__0",
|
||
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
|
||
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
|
||
"projection_inverse_Prims.Cons_a",
|
||
"projection_inverse_Prims.Cons_hd",
|
||
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
|
||
"subterm_ordering_Prims.Cons",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"typing_Catala.DefaultCalculus.empty_count",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_Catala.DefaultCalculus.typing_list",
|
||
"typing_tok_Catala.DefaultCalculus.AllEmpty@tok",
|
||
"typing_tok_Catala.DefaultCalculus.Conflict@tok", "unit_inversion",
|
||
"unit_typing"
|
||
],
|
||
0,
|
||
"c276ecd52a1dcec3934e865400780d2b"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.substitution_extensionnal",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_2",
|
||
"binder_x_458e1207db65a065f90af5aa9bc6edd7_1",
|
||
"binder_x_6c50c515b77925886e3faaa30943f0fb_0",
|
||
"constructor_distinct_Catala.DefaultCalculus.EApp",
|
||
"constructor_distinct_Catala.DefaultCalculus.EDefault",
|
||
"constructor_distinct_Catala.DefaultCalculus.EIf",
|
||
"constructor_distinct_Catala.DefaultCalculus.ELit",
|
||
"constructor_distinct_Catala.DefaultCalculus.EVar",
|
||
"disc_equation_Catala.DefaultCalculus.EAbs",
|
||
"disc_equation_Catala.DefaultCalculus.EApp",
|
||
"disc_equation_Catala.DefaultCalculus.EDefault",
|
||
"disc_equation_Catala.DefaultCalculus.EIf",
|
||
"disc_equation_Catala.DefaultCalculus.ELit",
|
||
"disc_equation_Catala.DefaultCalculus.EVar",
|
||
"equation_Catala.DefaultCalculus.var",
|
||
"equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst_abs.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"function_token_typing_Prims.__cache_version_number__",
|
||
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
|
||
"primitive_Prims.op_Subtraction",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_fn",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_tau_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_bfalse",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_btrue",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_test",
|
||
"projection_inverse_Catala.DefaultCalculus.ELit_l",
|
||
"projection_inverse_Catala.DefaultCalculus.EVar_v",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"refinement_interpretation_Tm_refine_e34d62365b53d6f78f1144ed17941a7b",
|
||
"subterm_ordering_Catala.DefaultCalculus.EAbs",
|
||
"subterm_ordering_Catala.DefaultCalculus.EApp",
|
||
"subterm_ordering_Catala.DefaultCalculus.EDefault",
|
||
"subterm_ordering_Catala.DefaultCalculus.EIf",
|
||
"token_correspondence_Catala.DefaultCalculus.subst_abs",
|
||
"true_interp"
|
||
],
|
||
0,
|
||
"f5242e01fdb2ece7a83caa64523ecd2a"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.substitution_extensionnal",
|
||
2,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@query", "binder_x_374a7fe1e57403f158e71980a97ecb0e_2",
|
||
"binder_x_458e1207db65a065f90af5aa9bc6edd7_1",
|
||
"binder_x_6c50c515b77925886e3faaa30943f0fb_0",
|
||
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"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_e34d62365b53d6f78f1144ed17941a7b",
|
||
"subterm_ordering_Prims.Cons"
|
||
],
|
||
0,
|
||
"01210c300d902daad597be384d236e96"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.subst_typing",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
|
||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||
],
|
||
0,
|
||
"17d57ea9dcdbf3e5529ae5c016b6e267"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.substitution_preserves_typing",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst_abs.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_16e47229fa4f513e4aff966f842aa522",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_5153a86c3b84f2f129d4da674d5d28c1",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
|
||
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"assumption_Catala.DefaultCalculus.ty__uu___haseq",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_1",
|
||
"binder_x_5fb06af9e7383e6ae83424b64f7b9e82_0",
|
||
"binder_x_5fb06af9e7383e6ae83424b64f7b9e82_4",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_2",
|
||
"binder_x_6c50c515b77925886e3faaa30943f0fb_3", "bool_inversion",
|
||
"bool_typing", "constructor_distinct_Catala.DefaultCalculus.EAbs",
|
||
"constructor_distinct_Catala.DefaultCalculus.EApp",
|
||
"constructor_distinct_Catala.DefaultCalculus.EDefault",
|
||
"constructor_distinct_Catala.DefaultCalculus.EIf",
|
||
"constructor_distinct_Catala.DefaultCalculus.ELit",
|
||
"constructor_distinct_Catala.DefaultCalculus.EVar",
|
||
"constructor_distinct_Catala.DefaultCalculus.TArrow",
|
||
"constructor_distinct_FStar.Pervasives.Native.Some",
|
||
"data_elim_Catala.DefaultCalculus.EVar",
|
||
"data_elim_FStar.Pervasives.Native.Some",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"disc_equation_Catala.DefaultCalculus.EAbs",
|
||
"disc_equation_Catala.DefaultCalculus.EApp",
|
||
"disc_equation_Catala.DefaultCalculus.EDefault",
|
||
"disc_equation_Catala.DefaultCalculus.EIf",
|
||
"disc_equation_Catala.DefaultCalculus.ELit",
|
||
"disc_equation_Catala.DefaultCalculus.EVar",
|
||
"disc_equation_Catala.DefaultCalculus.TArrow",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"equality_tok_Catala.DefaultCalculus.TBool@tok",
|
||
"equation_Catala.DefaultCalculus.env",
|
||
"equation_Catala.DefaultCalculus.extend",
|
||
"equation_Catala.DefaultCalculus.increment",
|
||
"equation_Catala.DefaultCalculus.is_renaming_prop",
|
||
"equation_Catala.DefaultCalculus.is_renaming_size",
|
||
"equation_Catala.DefaultCalculus.is_var_size",
|
||
"equation_Catala.DefaultCalculus.var",
|
||
"equation_Catala.DefaultCalculus.var_to_exp",
|
||
"equation_FStar.FunctionalExtensionality.feq",
|
||
"equation_FStar.FunctionalExtensionality.restricted_t",
|
||
"equation_Prims.nat", "equation_Prims.prop",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst_abs.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.lit",
|
||
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
|
||
"fuel_token_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented_token",
|
||
"function_token_typing_Catala.DefaultCalculus.extend",
|
||
"function_token_typing_Catala.DefaultCalculus.subst_abs",
|
||
"function_token_typing_Prims.__cache_version_number__",
|
||
"int_inversion", "int_typing",
|
||
"interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"interpretation_Tm_abs_9b0fb98b88819d883b74246421860dc1",
|
||
"lemma_Catala.DefaultCalculus.substitution_extensionnal",
|
||
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
|
||
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
|
||
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
|
||
"primitive_Prims.op_disEquality",
|
||
"proj_equation_FStar.Pervasives.Native.Some_v",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_BoxInt_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EAbs_body",
|
||
"projection_inverse_Catala.DefaultCalculus.EAbs_vty",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_fn",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_tau_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_bfalse",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_btrue",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_test",
|
||
"projection_inverse_Catala.DefaultCalculus.ELit_l",
|
||
"projection_inverse_Catala.DefaultCalculus.EVar_v",
|
||
"projection_inverse_Catala.DefaultCalculus.TArrow_tin",
|
||
"projection_inverse_Catala.DefaultCalculus.TArrow_tout",
|
||
"projection_inverse_FStar.Pervasives.Native.Some_a",
|
||
"projection_inverse_FStar.Pervasives.Native.Some_v",
|
||
"refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
|
||
"refinement_interpretation_Tm_refine_4572a4f2c61a47ef86084a21730a7db0",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"refinement_interpretation_Tm_refine_73f210ca6e0061ed4a3150f69b8f33bf",
|
||
"refinement_interpretation_Tm_refine_796ea366a949e0b57c08263b6d4daad3",
|
||
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
|
||
"refinement_interpretation_Tm_refine_bcced13304791c2e1ef0eb3c0488e66c",
|
||
"refinement_interpretation_Tm_refine_d67758a13faa7f83563fc253808b2c51",
|
||
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"subterm_ordering_Catala.DefaultCalculus.EAbs",
|
||
"subterm_ordering_Catala.DefaultCalculus.EApp",
|
||
"subterm_ordering_Catala.DefaultCalculus.EDefault",
|
||
"subterm_ordering_Catala.DefaultCalculus.EIf",
|
||
"token_correspondence_Catala.DefaultCalculus.subst_abs",
|
||
"token_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"typing_Catala.DefaultCalculus.extend",
|
||
"typing_Catala.DefaultCalculus.increment",
|
||
"typing_Catala.DefaultCalculus.is_renaming_prop",
|
||
"typing_Catala.DefaultCalculus.is_renaming_size",
|
||
"typing_Catala.DefaultCalculus.is_var_size",
|
||
"typing_Catala.DefaultCalculus.subst",
|
||
"typing_Catala.DefaultCalculus.subst_abs",
|
||
"typing_Catala.DefaultCalculus.subst_list",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_Catala.DefaultCalculus.typing_list",
|
||
"typing_Catala.DefaultCalculus.uu___is_EVar",
|
||
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
|
||
"typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"typing_Tm_abs_9b0fb98b88819d883b74246421860dc1",
|
||
"typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion",
|
||
"unit_typing", "well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"aa3a6a24f4728c912a06d82c99426292"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.substitution_preserves_typing",
|
||
2,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"binder_x_374a7fe1e57403f158e71980a97ecb0e_1",
|
||
"binder_x_5fb06af9e7383e6ae83424b64f7b9e82_0",
|
||
"binder_x_5fb06af9e7383e6ae83424b64f7b9e82_4",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_2",
|
||
"binder_x_6c50c515b77925886e3faaa30943f0fb_3", "bool_inversion",
|
||
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
|
||
"constructor_distinct_Tm_unit", "disc_equation_Prims.Cons",
|
||
"disc_equation_Prims.Nil",
|
||
"equation_Catala.DefaultCalculus.is_var_size",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.subst_list.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"function_token_typing_Prims.__cache_version_number__", "int_typing",
|
||
"primitive_Prims.op_AmpAmp", "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", "projection_inverse_Prims.Nil_a",
|
||
"refinement_interpretation_Tm_refine_4572a4f2c61a47ef86084a21730a7db0",
|
||
"subterm_ordering_Prims.Cons",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"typing_Catala.DefaultCalculus.is_var_size",
|
||
"typing_Catala.DefaultCalculus.subst",
|
||
"typing_Catala.DefaultCalculus.subst_list",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_Catala.DefaultCalculus.typing_list",
|
||
"well-founded-ordering-on-nat"
|
||
],
|
||
0,
|
||
"c519c453b0f1a9388f56d0535bc50cb3"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.preservation",
|
||
1,
|
||
3,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
|
||
"equation_Prims.squash", "l_and-interp",
|
||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||
],
|
||
0,
|
||
"3bf4fe76ba9dfb3c52e3ed63de7adcae"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.preservation",
|
||
2,
|
||
3,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.empty_count.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_app.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_default.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_if.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_0d43cd04dcb6adc76343f25ff3f92639",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_16e47229fa4f513e4aff966f842aa522",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_5401141756166ef64ba94940663272f3",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841",
|
||
"Catala.DefaultCalculus_interpretation_Tm_arrow_89d0b3d44c0d7d897277e5ab0495686d",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Catala.DefaultCalculus_pretyping_287308be9a2dd6fe272526e35f960e02",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
|
||
"FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250",
|
||
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
|
||
"Prims_pretyping_ae567c2fb75be05905677af440075565",
|
||
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
|
||
"binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_1", "bool_inversion",
|
||
"bool_typing",
|
||
"constructor_distinct_Catala.DefaultCalculus.AllEmpty",
|
||
"constructor_distinct_Catala.DefaultCalculus.Conflict",
|
||
"constructor_distinct_Catala.DefaultCalculus.EAbs",
|
||
"constructor_distinct_Catala.DefaultCalculus.EApp",
|
||
"constructor_distinct_Catala.DefaultCalculus.EDefault",
|
||
"constructor_distinct_Catala.DefaultCalculus.EIf",
|
||
"constructor_distinct_Catala.DefaultCalculus.ELit",
|
||
"constructor_distinct_Catala.DefaultCalculus.EVar",
|
||
"constructor_distinct_Catala.DefaultCalculus.IllFormed",
|
||
"constructor_distinct_Catala.DefaultCalculus.LConflictError",
|
||
"constructor_distinct_Catala.DefaultCalculus.LEmptyError",
|
||
"constructor_distinct_Catala.DefaultCalculus.LTrue",
|
||
"constructor_distinct_Catala.DefaultCalculus.NoStep",
|
||
"constructor_distinct_Catala.DefaultCalculus.OneNonEmpty",
|
||
"constructor_distinct_Catala.DefaultCalculus.SomeStep",
|
||
"constructor_distinct_Catala.DefaultCalculus.TArrow",
|
||
"constructor_distinct_Catala.DefaultCalculus.TBool",
|
||
"constructor_distinct_Catala.DefaultCalculus.TUnit",
|
||
"constructor_distinct_Catala.DefaultCalculus.exceptions_count_result",
|
||
"constructor_distinct_FStar.Pervasives.Native.None",
|
||
"constructor_distinct_FStar.Pervasives.Native.Some",
|
||
"constructor_distinct_Prims.unit", "constructor_distinct_Tm_unit",
|
||
"data_elim_Catala.DefaultCalculus.EVar",
|
||
"data_elim_FStar.Pervasives.Native.Some",
|
||
"data_typing_intro_Catala.DefaultCalculus.TArrow@tok",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"disc_equation_Catala.DefaultCalculus.AllEmpty",
|
||
"disc_equation_Catala.DefaultCalculus.Conflict",
|
||
"disc_equation_Catala.DefaultCalculus.EAbs",
|
||
"disc_equation_Catala.DefaultCalculus.EApp",
|
||
"disc_equation_Catala.DefaultCalculus.EDefault",
|
||
"disc_equation_Catala.DefaultCalculus.EIf",
|
||
"disc_equation_Catala.DefaultCalculus.ELit",
|
||
"disc_equation_Catala.DefaultCalculus.EVar",
|
||
"disc_equation_Catala.DefaultCalculus.LConflictError",
|
||
"disc_equation_Catala.DefaultCalculus.LEmptyError",
|
||
"disc_equation_Catala.DefaultCalculus.LTrue",
|
||
"disc_equation_Catala.DefaultCalculus.OneNonEmpty",
|
||
"disc_equation_FStar.Pervasives.Native.None",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"disc_equation_Prims.Nil",
|
||
"equality_tok_Catala.DefaultCalculus.AllEmpty@tok",
|
||
"equality_tok_Catala.DefaultCalculus.Conflict@tok",
|
||
"equality_tok_Catala.DefaultCalculus.IllFormed@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LConflictError@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LEmptyError@tok",
|
||
"equality_tok_Catala.DefaultCalculus.LTrue@tok",
|
||
"equality_tok_Catala.DefaultCalculus.NoStep@tok",
|
||
"equality_tok_Catala.DefaultCalculus.TBool@tok",
|
||
"equality_tok_Catala.DefaultCalculus.TUnit@tok",
|
||
"equation_Catala.DefaultCalculus.c_err",
|
||
"equation_Catala.DefaultCalculus.e_err",
|
||
"equation_Catala.DefaultCalculus.empty",
|
||
"equation_Catala.DefaultCalculus.env",
|
||
"equation_Catala.DefaultCalculus.extend",
|
||
"equation_Catala.DefaultCalculus.is_value",
|
||
"equation_Catala.DefaultCalculus.var",
|
||
"equation_Catala.DefaultCalculus.var_to_exp",
|
||
"equation_Catala.DefaultCalculus.var_to_exp_beta",
|
||
"equation_FStar.FunctionalExtensionality.feq",
|
||
"equation_FStar.FunctionalExtensionality.restricted_t",
|
||
"equation_Prims.l_and", "equation_Prims.nat",
|
||
"equation_Prims.squash",
|
||
"equation_with_fuel_Catala.DefaultCalculus.empty_count.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_app.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_default.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_exceptions.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_if.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.lit",
|
||
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"function_token_typing_Catala.DefaultCalculus.extend",
|
||
"function_token_typing_Catala.DefaultCalculus.is_value",
|
||
"function_token_typing_Catala.DefaultCalculus.var_to_exp_beta",
|
||
"function_token_typing_Prims.__cache_version_number__",
|
||
"int_inversion",
|
||
"interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af",
|
||
"interpretation_Tm_abs_88a3eeb445d1bcada942dc04cac3e8d7",
|
||
"interpretation_Tm_abs_9b0fb98b88819d883b74246421860dc1",
|
||
"kinding_Catala.DefaultCalculus.exp@tok", "l_and-interp",
|
||
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
|
||
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
|
||
"primitive_Prims.op_Equality", "primitive_Prims.op_Negation",
|
||
"proj_equation_Catala.DefaultCalculus.ELit_l",
|
||
"proj_equation_FStar.Pervasives.Native.Some_v",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EAbs_body",
|
||
"projection_inverse_Catala.DefaultCalculus.EAbs_vty",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_fn",
|
||
"projection_inverse_Catala.DefaultCalculus.EApp_tau_arg",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_bfalse",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_btrue",
|
||
"projection_inverse_Catala.DefaultCalculus.EIf_test",
|
||
"projection_inverse_Catala.DefaultCalculus.ELit_l",
|
||
"projection_inverse_Catala.DefaultCalculus.EVar_v",
|
||
"projection_inverse_Catala.DefaultCalculus.OneNonEmpty__0",
|
||
"projection_inverse_Catala.DefaultCalculus.SomeStep__0",
|
||
"projection_inverse_Catala.DefaultCalculus.TArrow_tin",
|
||
"projection_inverse_Catala.DefaultCalculus.TArrow_tout",
|
||
"projection_inverse_FStar.Pervasives.Native.Some_v",
|
||
"refinement_interpretation_Tm_refine_1f79706984431459041a6f7851223328",
|
||
"refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084",
|
||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
|
||
"refinement_interpretation_Tm_refine_4572a4f2c61a47ef86084a21730a7db0",
|
||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"refinement_interpretation_Tm_refine_6ccee90986879ff2274b72e5bc3434cf",
|
||
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
|
||
"refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be",
|
||
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
|
||
"subterm_ordering_Catala.DefaultCalculus.EApp",
|
||
"subterm_ordering_Catala.DefaultCalculus.EDefault",
|
||
"subterm_ordering_Catala.DefaultCalculus.EIf",
|
||
"token_correspondence_Catala.DefaultCalculus.extend",
|
||
"token_correspondence_Catala.DefaultCalculus.step_exceptions.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.var_to_exp_beta",
|
||
"typing_Catala.DefaultCalculus.__proj__ELit__item__l",
|
||
"typing_Catala.DefaultCalculus.empty",
|
||
"typing_Catala.DefaultCalculus.is_value",
|
||
"typing_Catala.DefaultCalculus.step",
|
||
"typing_Catala.DefaultCalculus.subst",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_Catala.DefaultCalculus.uu___is_ELit",
|
||
"typing_Catala.DefaultCalculus.var_to_exp_beta",
|
||
"typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a",
|
||
"typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af",
|
||
"typing_Tm_abs_9b0fb98b88819d883b74246421860dc1",
|
||
"typing_tok_Catala.DefaultCalculus.AllEmpty@tok",
|
||
"typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion",
|
||
"unit_typing"
|
||
],
|
||
0,
|
||
"1e47a11fea34c5c271443a4b0f90e428"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.preservation",
|
||
3,
|
||
3,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
|
||
"equation_Prims.squash", "l_and-interp",
|
||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||
],
|
||
0,
|
||
"0e7a6af020959c58c04caab0a14b1921"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.preservation",
|
||
4,
|
||
3,
|
||
1,
|
||
[
|
||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"@query",
|
||
"Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688",
|
||
"Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3",
|
||
"b2t_def", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0",
|
||
"binder_x_57403813bce408351cc0e70737e314ef_1",
|
||
"binder_x_6aa41574d40712b03e0367a1a3c256b3_4",
|
||
"binder_x_9d898a02527d03c282f289aa9ecae7fc_2",
|
||
"binder_x_9d898a02527d03c282f289aa9ecae7fc_3", "bool_inversion",
|
||
"bool_typing",
|
||
"constructor_distinct_Catala.DefaultCalculus.EDefault",
|
||
"constructor_distinct_Catala.DefaultCalculus.ELit",
|
||
"constructor_distinct_Catala.DefaultCalculus.LConflictError",
|
||
"constructor_distinct_FStar.Pervasives.Native.None",
|
||
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
|
||
"data_elim_Catala.DefaultCalculus.EDefault",
|
||
"data_elim_FStar.Pervasives.Native.Some",
|
||
"data_typing_intro_Catala.DefaultCalculus.EDefault@tok",
|
||
"data_typing_intro_Catala.DefaultCalculus.ELit@tok",
|
||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||
"disc_equation_FStar.Pervasives.Native.None",
|
||
"disc_equation_FStar.Pervasives.Native.Some",
|
||
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
|
||
"equality_tok_Catala.DefaultCalculus.LConflictError@tok",
|
||
"equality_tok_Catala.DefaultCalculus.TBool@tok",
|
||
"equation_Catala.DefaultCalculus.c_err",
|
||
"equation_Catala.DefaultCalculus.empty",
|
||
"equation_Catala.DefaultCalculus.is_value", "equation_Prims.l_and",
|
||
"equation_Prims.squash",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"fuel_guarded_inversion_Catala.DefaultCalculus.exp",
|
||
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
|
||
"fuel_guarded_inversion_Prims.list",
|
||
"kinding_Catala.DefaultCalculus.exp@tok", "l_and-interp",
|
||
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
|
||
"primitive_Prims.op_Equality",
|
||
"proj_equation_FStar.Pervasives.Native.Some_v",
|
||
"projection_inverse_BoxBool_proj_0",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_cons",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_exceptions",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||
"projection_inverse_Catala.DefaultCalculus.ELit_l",
|
||
"projection_inverse_FStar.Pervasives.Native.Some_v",
|
||
"projection_inverse_Prims.Cons_a",
|
||
"projection_inverse_Prims.Cons_hd",
|
||
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
|
||
"refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084",
|
||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
|
||
"refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be",
|
||
"refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14",
|
||
"refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1",
|
||
"subterm_ordering_Prims.Cons",
|
||
"token_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||
"typing_Catala.DefaultCalculus.empty",
|
||
"typing_Catala.DefaultCalculus.step",
|
||
"typing_Catala.DefaultCalculus.step_exceptions_left_to_right",
|
||
"typing_Catala.DefaultCalculus.typing",
|
||
"typing_tok_Catala.DefaultCalculus.LConflictError@tok",
|
||
"typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion",
|
||
"unit_typing"
|
||
],
|
||
0,
|
||
"8027f16b03d414235a16bb198765a509"
|
||
]
|
||
]
|
||
] |