mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-19 16:28:12 +03:00
1657 lines
77 KiB
Plaintext
Generated
1657 lines
77 KiB
Plaintext
Generated
[
|
||
"^ÖÒ\u0019æ<39>œ¦R³ïi¨\n\u001c6",
|
||
[
|
||
[
|
||
"Catala.DefaultCalculus.ty",
|
||
1,
|
||
2,
|
||
1,
|
||
[ "@query" ],
|
||
0,
|
||
"f9fc150dd19183938eeb34ba6bdbd657"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__TArrow__item__tin",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee"
|
||
],
|
||
0,
|
||
"f3d2b8f547abda0782f87d707c869b8d"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__TArrow__item__tout",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee"
|
||
],
|
||
0,
|
||
"ae852addd65be90b335b6bb218cd95e5"
|
||
],
|
||
[
|
||
"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,
|
||
"9d2a37207e7e44a0aa6f895ac36f1711"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EVar__item__v",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_f7bcdc7958786fcb60dfc7f410094686"
|
||
],
|
||
0,
|
||
"05f351ca93ca78b5c20d9328736cafe5"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EApp__item__fn",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||
],
|
||
0,
|
||
"78ec509aeb281285063fdd61420f514c"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EApp__item__arg",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||
],
|
||
0,
|
||
"32f71b14277a31a4820bb616728f3bd2"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EApp__item__tau_arg",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||
],
|
||
0,
|
||
"fd0ed4fe677d8fede0d42bcbc67941cd"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EAbs__item__vty",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5"
|
||
],
|
||
0,
|
||
"7826102b160ea54aa1f02dd7f88fa29d"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EAbs__item__body",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5"
|
||
],
|
||
0,
|
||
"7075e86600a1b931d7638df53c3d7644"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__ELit__item__l",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_6ccee90986879ff2274b72e5bc3434cf"
|
||
],
|
||
0,
|
||
"1fb7b5d0d6bbc1c9f454281a01f5d2e5"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EIf__item__test",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||
],
|
||
0,
|
||
"e0826990f2bf12b896b259ea7a29ef9c"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EIf__item__btrue",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||
],
|
||
0,
|
||
"3e0b50e34c3d0856d8063655fa3c78b9"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EIf__item__bfalse",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||
],
|
||
0,
|
||
"abe0700812430ee14bee827a916c4c36"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__exceptions",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"2c8da04378b45ddc9e70997245b3d392"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__just",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"71722c3137aef8a070db92954483c125"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__cons",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"c9b5aa06f3d4f96ce9c2dd3b36b4e95e"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__EDefault__item__tau",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||
],
|
||
0,
|
||
"fc5a0984f34fcd69654e5047e1be4a72"
|
||
],
|
||
[
|
||
"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,
|
||
"47c120cc648999657f8b75f2e0dbf98d"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.is_renaming_size",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_1c1d1c6e28a4d07ae30d44381ee0d524"
|
||
],
|
||
0,
|
||
"1646f35ef9996dc3507029920875e4cb"
|
||
],
|
||
[
|
||
"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,
|
||
"58c826601d51afd33df888b64778cf63"
|
||
],
|
||
[
|
||
"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,
|
||
"a33ba95b81f3dfeb49bb013dce518b46"
|
||
],
|
||
[
|
||
"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,
|
||
"d204a4c04ff4bc41a8e408f2c793af32"
|
||
],
|
||
[
|
||
"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,
|
||
"f33db5ddb71da97242c740564a00705e"
|
||
],
|
||
[
|
||
"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,
|
||
"999f67f38fe11e22b56ff48356f22e05"
|
||
],
|
||
[
|
||
"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,
|
||
"dfbbef2a7fec7f91a01db5caddc3f504"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.empty_count_result",
|
||
1,
|
||
2,
|
||
1,
|
||
[ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ],
|
||
0,
|
||
"454de250dadf437ce9064f8c2faea487"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__OneNonEmpty__item___0",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_73db3433a5536656aa27657eb477efcf"
|
||
],
|
||
0,
|
||
"ae7f3ffcfdaa53938d6fe23884ff4317"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.exceptions_count_result",
|
||
1,
|
||
2,
|
||
1,
|
||
[ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ],
|
||
0,
|
||
"3bbdf3db8159f245ce2f2b1c10d6f185"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.__proj__SomeStep__item___0",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query",
|
||
"refinement_interpretation_Tm_refine_562b75d472a96c36a24c70375d81f26c"
|
||
],
|
||
0,
|
||
"f118d5761b19e05ce48da02ba76c2f6b"
|
||
],
|
||
[
|
||
"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,
|
||
"f6427a407f48df6b59262b4edde385d8"
|
||
],
|
||
[
|
||
"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,
|
||
"bc2f87497f995ee90a31614799faef5d"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.step_app",
|
||
2,
|
||
2,
|
||
1,
|
||
[
|
||
"@query", "kinding_Catala.DefaultCalculus.exp@tok",
|
||
"lemma_FStar.Pervasives.invertOption"
|
||
],
|
||
0,
|
||
"b11c90217682aba8d32a382aa9725984"
|
||
],
|
||
[
|
||
"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,
|
||
"24f79481280d552251146950686604be"
|
||
],
|
||
[
|
||
"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,
|
||
"0b662622406376d0a2bd18937e18ed5e"
|
||
],
|
||
[
|
||
"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,
|
||
"0d237febd87140396125c39c4ddc415b"
|
||
],
|
||
[
|
||
"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,
|
||
"0cd9555520b3ca27b77b9ee22f77a1a3"
|
||
],
|
||
[
|
||
"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,
|
||
"b4d7124ea3722a753e1998e8e1c6eb80"
|
||
],
|
||
[
|
||
"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,
|
||
"0cab940a4adca30ec6c107f4bd65ab7e"
|
||
],
|
||
[
|
||
"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,
|
||
"4e3b314f9599171e039bda02fbe32288"
|
||
],
|
||
[
|
||
"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,
|
||
"96fcf67d7e9d68c08815d5b863cc5d75"
|
||
],
|
||
[
|
||
"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,
|
||
"26ee0e9ab80a19918e4ab06c7aee8d1d"
|
||
],
|
||
[
|
||
"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,
|
||
"dd491009ff9878ade2d35c8a0b85322d"
|
||
],
|
||
[
|
||
"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,
|
||
"679a7f3e7e17536eec0ea6f54aff9c71"
|
||
],
|
||
[
|
||
"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,
|
||
"08a419c32cc4a72f098d5ba10436fdfc"
|
||
],
|
||
[
|
||
"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,
|
||
"244f9100ad5c28fa85f738e2670fd162"
|
||
],
|
||
[
|
||
"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,
|
||
"988376e56f3be5f5faa5177a5f4bce4b"
|
||
],
|
||
[
|
||
"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,
|
||
"9fccb768658c208db732cb784b5ae99a"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.subst_typing",
|
||
1,
|
||
2,
|
||
1,
|
||
[
|
||
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
|
||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||
],
|
||
0,
|
||
"a9581b31b098f8c6ed0c28a5af28af64"
|
||
],
|
||
[
|
||
"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,
|
||
"17d841d14a1131d163065fbd7aabaaba"
|
||
],
|
||
[
|
||
"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,
|
||
"b393907a80bc0e092e77f702ffaf264a"
|
||
],
|
||
[
|
||
"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,
|
||
"2caf5bf722b94a214563c4b58dfd0592"
|
||
],
|
||
[
|
||
"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,
|
||
"1f5c06cb5572febc9e2355e796f50834"
|
||
],
|
||
[
|
||
"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,
|
||
"b3bcc3a1d16fea99e6f6a223fe293e0f"
|
||
],
|
||
[
|
||
"Catala.DefaultCalculus.preservation",
|
||
4,
|
||
4,
|
||
2,
|
||
[
|
||
"@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.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.None_a",
|
||
"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_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.TBool@tok", "unit_inversion",
|
||
"unit_typing"
|
||
],
|
||
0,
|
||
"0ffcc137baddae54cd5223d99bb5fffa"
|
||
]
|
||
]
|
||
] |