itp_interface/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/agent/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/agent/simple_proof_agent.py,sha256=mk2YBM9AKEoEZtmFbvU0f9I76BWXvdRHBDIuFSEd2vQ,4119
itp_interface/coq_ser_api/__init__.py,sha256=fHI4ZGgPPXKvWyv3_12ZlUBV22izjgnU4i4KtS-CgTg,7504
itp_interface/coq_ser_api/contexts.py,sha256=8jMV6E4UaabxenEA6PVICXxOey5oXunUXdlE0QMhRWI,11213
itp_interface/coq_ser_api/coq_agent.py,sha256=-GJ_5YvQ5Q1mZ0zTqMfWbgyGdaASGuQC0wMO1N1aRfs,17800
itp_interface/coq_ser_api/coq_backend.py,sha256=H96ps0iE7foicq63RvQZ6s9c5CvEwFZhagBwpFC1aAw,2456
itp_interface/coq_ser_api/coq_util.py,sha256=fo3xdrF_yij-4v-s0uJXg_zyNrQ6KPRrBRrTROCmAC8,32087
itp_interface/coq_ser_api/example.py,sha256=2iyMv-xJRAlkN-vfGzyQD3pYAqmvpZR9MECOIF_gnCg,2340
itp_interface/coq_ser_api/lsp_backend.py,sha256=RKlDiy3EyxXi79IqYOTTdRV7mfezMfAp4YST6gwbjJM,15920
itp_interface/coq_ser_api/py.typed,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/coq_ser_api/serapi_backend.py,sha256=eO55vWEMl4m-xkNeqz8Hv9_0GKxhHRlX2vxI7s8pBac,38242
itp_interface/coq_ser_api/util.py,sha256=CiQyFl3NSqev-EpB2JXXpIueN6zldl02qqg7deJpFpw,4017
itp_interface/lean/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/lean/lean4_local_data_extraction_transform.py,sha256=uk97d4I2mwJG48hfTW0psLL8m-u8UYk3ApTnm4ihGq0,17280
itp_interface/lean/parsing_helpers.py,sha256=SbWBOco1qCp3tVu_ITLxc_-iIj9GolLBCEcWS_-Yx-c,14143
itp_interface/lean/simple_lean4_sync_executor.py,sha256=aO7HroT8Fpbm8oflAW6xoeqU9tg9x-uTBWiaQnZGsHQ,57549
itp_interface/lean/tactic_parser.py,sha256=ErlCG70ORo3Ee6VwGBJiDU79ydM5rgi-rWmOBDdvhRk,38582
itp_interface/lean/tactic_parser/TacticParser.lean,sha256=wP4Ey2jfq-VUC837chaZ6LlJaVPhxeQGU8zQQ22G1XI,183
itp_interface/lean/tactic_parser/lake-manifest.json,sha256=aJpWg6J6IKtV1X5STDonAut2sq25NJDGo0D547WLezg,118
itp_interface/lean/tactic_parser/lakefile.toml,sha256=CtwKYd5TeLABCwaRl0j-MW0DCjqrmTkdKdJWv1z7Pio,486
itp_interface/lean/tactic_parser/lean-toolchain,sha256=3-gq1-2owvNyO1GV3l4_9nejKMfUS9RdR4-iO02KgQs,24
itp_interface/lean/tactic_parser/test_user_example.lean,sha256=o1fD0dcjBNbQnNqbKHcGh3lSbkBK36C-9nTgcSJLltM,671
itp_interface/lean/tactic_parser/TacticParser/Base64.lean,sha256=h0NSRflCogJWbh-dAR7_Nstz0hNz7gQL0SK_rIbhYss,2695
itp_interface/lean/tactic_parser/TacticParser/DependencyParser.lean,sha256=4_AmKKTwBb_YMdOqaTJVTQbSt6rFNNMFIWhWrFxzqW0,18164
itp_interface/lean/tactic_parser/TacticParser/DependencyParserMain.lean,sha256=VVv0YqAJic7W_36NI8a4174X-iBu0uPgw-WBjS4Xhxs,1194
itp_interface/lean/tactic_parser/TacticParser/LineParser.lean,sha256=HkFPnD6iL40d2440QP4XtHSwOLixXs2k8LETliK-hzY,17376
itp_interface/lean/tactic_parser/TacticParser/Main.lean,sha256=c2aYD8wcepH623TDfNA2MyUnZtHmuzCbnWX5t1rzimo,7656
itp_interface/lean/tactic_parser/TacticParser/ProofExtractor.lean,sha256=1njcI6qYpwMuu_RH34EI-PDEJGW6tHj5yZxYjaRp-Qw,7466
itp_interface/lean/tactic_parser/TacticParser/SyntaxWalker.lean,sha256=1I7oDce3YrXsdXqb6WtqlDXM5deSrHM-u1v1kkJ5zoE,17258
itp_interface/lean/tactic_parser/TacticParser/TacticExtractorMain.lean,sha256=YOcTNvcDBN01IT6G53NQdS5Ms4nq1Bzc0SvQ9AuKyHI,1440
itp_interface/lean/tactic_parser/TacticParser/Types.lean,sha256=_ONb-zSzVFhCwKwGpAnRjvXZCC62S9pF8EE6jbBDMP4,9259
itp_interface/lean/tactic_parser/TacticParser/Example/complex.lean,sha256=h0GbqWBGToDnhyFHr3VU88RRdT6YztUXfcDQvU87kOA,490
itp_interface/lean/tactic_parser/TacticParser/Example/simple.lean,sha256=ZrvjMXgxlOQ9Mf_pVl1pGsR2EszbzbRDDBwlfzzbVCk,272
itp_interface/lean_server/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/lean_server/commands.py,sha256=OxXT5MFPpk4VMRCb0Jleon4seQJsH3z7dGuyf_Fsu6c,11799
itp_interface/lean_server/lean3_search_tool.py,sha256=28KbIzEGI8tta-AtI_WoHWdS02EcRHW3zjrzorJT5Js,12731
itp_interface/lean_server/lean4_repl_interface.py,sha256=_vle7Ff6ySXE1CZRPvHpg0gEBtUcOGAe2626US0RGv4,6448
itp_interface/lean_server/lean4_utils.py,sha256=DR5fIbqL4Pj5-JtacRSyjkdiib0Xql3BuUes0MaF-sg,11238
itp_interface/lean_server/lean_cmd_server.py,sha256=bHEbQoGDn-JO3qR88EYt_xo1jSxDJVXryuIHtRUg2ic,4182
itp_interface/lean_server/lean_context.py,sha256=R2rxgCP8Eb6WPTpZDjiD7btxpz_tIKgG2Pdo_HqZzjQ,2029
itp_interface/lean_server/lean_sync_server.py,sha256=0wDAwfVMezsCCsC6TlofyqvX-YZJfbaT2DL4PbdshAo,6416
itp_interface/lean_server/lean_utils.py,sha256=RTDk_lLo_g7AySxep8_NgWGOBPzh02hfhAOlGcIkBBA,8315
itp_interface/lean_server/py.typed,sha256=8PjyZ1aVoQpRVvt71muvuq5qE-jTFZkK-GLHkhdebmc,26
itp_interface/main/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/config.py,sha256=5lvUAxU0H_v266UAk8UnAtuZq024g4L63Wipm5ZpsTk,7798
itp_interface/main/extract_benchmark_dataset.py,sha256=2W4qiNBfqZAuOvlWBu9dRLmuWw73hiTwsLOsHnxmLZM,4737
itp_interface/main/filter_dataset.py,sha256=i-f7DLSRHgDZt8hA9nY47zFQf5bwwp8F86r_1a_z1Hw,4413
itp_interface/main/init_ray.py,sha256=RiytXkh1Ghb1psuD9hXHNf4XlWeEOx1pSL0Ro_JYCdc,3182
itp_interface/main/install.py,sha256=aU-mzfaktHBX_DKlfTr4GCaRv8QpgvAIkTm134JOdVM,2937
itp_interface/main/merge_dataset.py,sha256=TDHGJCElZpfV6ZMSwNwMZ5EiEkfoNu1ckiXFqii_wAk,9835
itp_interface/main/run_tool.py,sha256=D-mP8fP2AQpTNE73ybolG3tooivKS2GHLiWa6zvCSxE,35906
itp_interface/main/run_tool_no_hydra.py,sha256=srOQRvxNNUp3ZNIMz2x3hukVH6oO2EoL1ArZcUw8qUk,6716
itp_interface/main/configs/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/afp_data_gen.yaml,sha256=bLaG5Klq0RTPYHYT0XZ8ZhIXqAMOivkvqK8nE97-0LE,400
itp_interface/main/configs/category_theory_data_gen.yaml,sha256=ifm8tZGsG7_S3QfSAhCyh4FfZ0ULsZ1uR5x9X8iLzNs,412
itp_interface/main/configs/category_theory_data_gen_random.yaml,sha256=kZy-yqp-vMnjUGNXfw5I_MPck3STkgavOz3pJavuw38,469
itp_interface/main/configs/compcert_data_gen_test.yaml,sha256=cJeD3ZumvZU1HB-wf08RR_cuzXqwOwIZ2qF7hn8GU64,353
itp_interface/main/configs/compcert_data_gen_train.yaml,sha256=_IvIKslmJaBdpQAX9d9VHVBzExRprC2RR-ETaHmzUcY,293
itp_interface/main/configs/experiments.yaml,sha256=lEo0y2JOzhqWWosz_Vmn63ZnsBrhC64wmvdh9xJOMGI,447
itp_interface/main/configs/geo_coq_data_gen.yaml,sha256=b8_YdIQgjNXtGvzWqjzv5KOCzUCcpKWZ8Zs8Ahp0VjU,392
itp_interface/main/configs/geo_coq_data_gen_random.yaml,sha256=ydbCe-OZcfRmtiFPW8sO8k8sZ8EdZx-g409dZTveziM,451
itp_interface/main/configs/leandojo_random_data_gen.yaml,sha256=RnQ9G8mT7DtE-6xrbC8UPNgT9jC9LAAUwD4OWnV6Fgo,452
itp_interface/main/configs/math_comp_data_gen.yaml,sha256=_1F-VI6BaVVjHxc9VecKcNsSIPYVKaTXttsoV25VIuQ,398
itp_interface/main/configs/math_comp_data_gen_random.yaml,sha256=zhUKe8a9cQnTpGChw90T0IHK4StIEpDbNDqx8HIzYTs,460
itp_interface/main/configs/mathlib_data_gen.yaml,sha256=f9YoZwwRslnvwTSGs39lFoYk6oNLrg7LwmkRoKx8750,418
itp_interface/main/configs/mathlib_lean_data_extract.yaml,sha256=1hm1IWQVHqPMo77O-vFLEc4FoTJJWJgfquvmUBXouy0,495
itp_interface/main/configs/simple_coq_data_gen.yaml,sha256=x4sGvTsm2gCgiCFHcSoGNLczzZQoQx4Fcvtiv59i0Pg,462
itp_interface/main/configs/simple_coq_data_gen_random.yaml,sha256=K4uyy9lws1VxJpGpIlKPP2eSVi4Qag0J_gaNuHeqD0Q,539
itp_interface/main/configs/simple_lean_data_extract.yaml,sha256=aVsfEbr8roqOO381WY5BiA3H1WB6V5oAdj1Nbat2_n8,492
itp_interface/main/configs/simple_lean_data_gen.yaml,sha256=FspYS1PjGfiogy7tFjllb9694sTqNNbqo2f8tVQSjsU,484
itp_interface/main/configs/simple_rl_lean_data_gen.yaml,sha256=--MgYSkTeGi2DcwgW81obQ_dtCXOgHSBv_4qDOYyEek,476
itp_interface/main/configs/stdlib_lean_data_extract.yaml,sha256=K1zXJY_-1WODqe_rorPocvrXzHQasV2btlAWjzhDU7o,493
itp_interface/main/configs/uni_math_data_gen.yaml,sha256=_rS_ckglFe9eSXLbZD9KAjskTIHsxUhAO67R98mTNws,394
itp_interface/main/configs/benchmark/CompCert.yaml,sha256=kjKxzyvrMMYASvRKtYool5DVUpnrzIHwdLGdn-n16NE,9507
itp_interface/main/configs/benchmark/GeoCoq.yaml,sha256=Qg2XoQLF5szjesbkruyip8NmEbdk3NDkU5ao-9MJjx0,40290
itp_interface/main/configs/benchmark/UniMath.yaml,sha256=Ds7-vBeLYz9kJiEJjT9CXuQL4mdTud9SRKOdxnD-7cM,114891
itp_interface/main/configs/benchmark/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/benchmark/afp_isabelle.yaml,sha256=JAYQTQ1lLpjWZWukRzu0L5ELjO7XRvKRgd0OVur6ZOc,1032894
itp_interface/main/configs/benchmark/agent_proverbot_hard.yaml,sha256=bjTE6YijeHYB5ywIl44W5lICXJk8RTu4ZCIMaxWjur0,8445
itp_interface/main/configs/benchmark/category-theory.yaml,sha256=l794XryNTlf_E3XNEnULK6lRqYpGGcRJw8iFfipGwsE,13100
itp_interface/main/configs/benchmark/compcert_118_subset.yaml,sha256=lwSWCyP-NBU638xPkQ8ZOI1-fdHZmDORFLRCaJNCmBo,4538
itp_interface/main/configs/benchmark/compcert_benchmark.yaml,sha256=pwhSii0v01iRe6vgfo5hB8-MgEYRaj10AmneVK61yFA,1196
itp_interface/main/configs/benchmark/compcert_benchmark_hard.yaml,sha256=-QHhSAPdDTOdUSXVJbJ7jd9USQzGKElGhsFtkGb4BcI,16183
itp_interface/main/configs/benchmark/compcert_benchmark_hard_1.yaml,sha256=EQRRgt0tFJaOf9Hf5FaHQPndgc-cQwq1X-AWT9Y1XUI,1723
itp_interface/main/configs/benchmark/compcert_benchmark_hard_2.yaml,sha256=Negvm2d7kMBxYdzHzF6VdC5-0oaL_Mlq98zRBekL1LA,872
itp_interface/main/configs/benchmark/compcert_benchmark_hard_3.yaml,sha256=4iC__e2YVNizMApS6kuasMLmIFEQVtf-n1_SwCgYucw,3312
itp_interface/main/configs/benchmark/compcert_benchmark_hard_7_per_cent.yaml,sha256=srlzxmf0XvFux4K9xBVvI1CV99VpXuAH-f5nTj3zAqM,2542
itp_interface/main/configs/benchmark/compcert_benchmark_test.yaml,sha256=R9jOzWDzLczP1MA5yJPjZbU5ChFbQ1ZnFMbj9xwKj48,1257
itp_interface/main/configs/benchmark/compcert_benchmark_train.yaml,sha256=5ANOdYPdhXQz2qXDQ4r9pb0lcSHUyhGTwnuPp18BcVA,9857
itp_interface/main/configs/benchmark/leandojo_novel_premises_test.yaml,sha256=BU-1DgeM6rlTiY9pvvrbvfd7XL1FMaoOTI-Uqcd-l4A,104295
itp_interface/main/configs/benchmark/leandojo_novel_premises_train.yaml,sha256=zpPA_0ws3GB-fiz0NGWtv7w7LzWovIcJb_akP_Sq3c4,3913741
itp_interface/main/configs/benchmark/leandojo_novel_premises_val.yaml,sha256=LK8JTP8TH3f_ppj2ez5HJ7iegUdA0EpwW7EBxeRl9bM,103891
itp_interface/main/configs/benchmark/leandojo_random.yaml,sha256=ic5sS9VaQOZxVlutN9gDLh1i5N6pt0M9cGDSznfZeUQ,132832
itp_interface/main/configs/benchmark/leandojo_random_test.yaml,sha256=2akL6l4OZ1AkSv9jAWzFbEuEZCQBDi8k0ijyM9Kb1cU,100268
itp_interface/main/configs/benchmark/leandojo_random_train.yaml,sha256=zq3Qzg_tQrSZDFpHRQZUjLrJconmIwcGFMfh59mqDVo,2424463
itp_interface/main/configs/benchmark/leandojo_random_val.yaml,sha256=0S2VVepyhEXT_i-kCXDYQ0FkCkgHLi4lf5lvnJAQSBY,104293
itp_interface/main/configs/benchmark/math-comp.yaml,sha256=PXnxWCAumkoslxUBBItrpv9xlR5xxCCR0ZdzLKhUwzI,6037
itp_interface/main/configs/benchmark/mathlib_benchmark_lean_ext.yaml,sha256=EVSAlwY_aFXCQGPtVcu7lREzKdXR4vvzuKGYKwN1dP8,1993
itp_interface/main/configs/benchmark/miniF2F_test.yaml,sha256=SUdQncXJ30h1LZ45Wmz0NQrTyBuvylCmIQMLobgtOrE,302
itp_interface/main/configs/benchmark/miniF2F_test_aime.yaml,sha256=tLlkAtYbsSXDLxNzTxUXXUt8ClP-4jnEuBsrtAH5X-A,649
itp_interface/main/configs/benchmark/miniF2F_test_algebra.yaml,sha256=Q6DmDwBZX31wQJULvhF0gVjhOMloso1fLI1lBP8QqOc,1209
itp_interface/main/configs/benchmark/miniF2F_test_amc12.yaml,sha256=LZ0X3CWjMFZCOzULEWri3KGhHoN4fpQITQ5BoImYwRM,1444
itp_interface/main/configs/benchmark/miniF2F_test_few_shot_hard.yaml,sha256=W_GUIDAS7alFN3uTPURMuEixaT6tq4-ILCb9SLQMlEw,7592
itp_interface/main/configs/benchmark/miniF2F_test_imo.yaml,sha256=qxg5BTacMdiALoNNkajydf8Guqfp910kAane_DT_lNc,793
itp_interface/main/configs/benchmark/miniF2F_test_induction.yaml,sha256=9kBUKJXZSKDiTtMJKJDvPM92f0LGV7CIKQXf8aN8D-o,626
itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra.yaml,sha256=RVP9vygleL0RVeXPMk7QHq53SeHkKAq9H5Op6X_Twyw,2405
itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra_hard.yaml,sha256=Pp5lhSibhcKJt5RiAlHwQoe9GTJUhgj7a1Fy2MuS0LM,2111
itp_interface/main/configs/benchmark/miniF2F_test_mathd_numbertheory.yaml,sha256=PZHQcaVVT8o1YyucHnqtK_3NgXlgIVSRDs-aGuXniZM,2408
itp_interface/main/configs/benchmark/miniF2F_test_numbertheory.yaml,sha256=HejMgDRqhr5CjO9Z8BY66vjqM9Yo7tDxJraaHnBVo-U,698
itp_interface/main/configs/benchmark/minicompcert_benchmark_1.yaml,sha256=jLguBEzySX2h3m8THMqyCniF120FLhW3Ot7RWKCsJdE,552
itp_interface/main/configs/benchmark/proverbot_hard.yaml,sha256=S8MCygnq-s1gFBa9bFL9yRk55_rXEd8Rp7ugO_Uu9OQ,3160
itp_interface/main/configs/benchmark/re_prover.yaml,sha256=G1Bh8HLdRLB2FncCpSIQk1k8H4kNmmou1YnPc1Lc5do,1992
itp_interface/main/configs/benchmark/re_prover_hard.yaml,sha256=ofMOaf0pv-Op0qdXPrlXww7JcKweW3aF1iMI-VsXkMM,1206
itp_interface/main/configs/benchmark/re_prover_very_hard.yaml,sha256=1223tuC0ol5d3q9143DsrHZbmS862s2Rggult_h-AQU,617
itp_interface/main/configs/benchmark/reprover_with_retrieval.yaml,sha256=8Q-y_BasSDeLd3Gyqs573qn6EP7JAwBpqXHj52XqjvM,2240
itp_interface/main/configs/benchmark/reprover_with_retrieval_hard.yaml,sha256=1YNC2Rb57lShuKkrtGFR3TIUfWdkukT2-JiwItK3yh0,901
itp_interface/main/configs/benchmark/reprover_with_retrieval_neg.yaml,sha256=CsBOArbvK285dX1__DpobmVRDbkZjnNPBKpyD-YNM5g,6285
itp_interface/main/configs/benchmark/simple_benchmark_1.yaml,sha256=hb_3_k23FUYVHjNjoKtu23kXTrczY3c9kbxhlTXefhI,872
itp_interface/main/configs/benchmark/simple_benchmark_8.yaml,sha256=9WlLJaYV-zHEu7W4e8K8nQyJKZZNnSdeGSqMnoQnCoA,1349
itp_interface/main/configs/benchmark/simple_benchmark_9.yaml,sha256=K738uKF-RMeHXrryh43hak9HUC3p_2tushLQOkYyTss,1974
itp_interface/main/configs/benchmark/simple_benchmark_isabelle.yaml,sha256=UP9AX0kbHid0HqZYbmdIu6nKcoYESbCO4p3_HZTl1Vs,519
itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml,sha256=QT6sf7mDrMD9N6-9m7572z2MfBl_XI7-3Zasb1flCXg,318
itp_interface/main/configs/benchmark/simple_benchmark_lean_ext.yaml,sha256=MVzfvUU0VFaITobEhnNmwPzB2uR1FoCHmLRv7m72z4Y,354
itp_interface/main/configs/benchmark/simple_benchmark_lean_training_data.yaml,sha256=ZPCNaoYJzcn2UmxMm0C6FkfBt2njdm9NvrqkdtQL6xU,328
itp_interface/main/configs/benchmark/simple_rl_benchmark_lean.yaml,sha256=iX4VpPsGBlG0aHv3AQWeRE71QH2RNqFGu5SvXcC3YVE,425
itp_interface/main/configs/benchmark/stack_machine.yaml,sha256=tfqJJW5oPt5qatUQyspxwMXEaMly2jeN1kz-QdkaGJ4,347
itp_interface/main/configs/benchmark/stack_machine_hard.yaml,sha256=8J3iKNPEkKOLLMNLSv9vg5CDaffRYYylmVrVrxVElWU,406
itp_interface/main/configs/benchmark/stdlib_benchmark_lean_ext.yaml,sha256=upX4X8SaSARgWHkWwLDmE8ibYbLL8RMjcWGboyKRDd4,1152
itp_interface/main/configs/env_settings/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/env_settings/bm25_retrieval.yaml,sha256=QJ7X2Di82atJ5rnCSm06B6gkH7pw5yvNxHEbhfccshg,45
itp_interface/main/configs/env_settings/bm25_retrieval_no_dfns.yaml,sha256=NPo-e989ztHdouLivnhrm66shkuhDh4Pomd8joFbGBY,61
itp_interface/main/configs/env_settings/bm25_retrieval_only_local_no_dfns.yaml,sha256=1yZiRn7280k2GeZmUAIvHudMNfunYyX_JImgUiJ2RQU,83
itp_interface/main/configs/env_settings/bm25_retrieval_with_print.yaml,sha256=7P_PBJzDt_w9fLFeac6h2-lwv2x7D32bbM6gdJc7Ywo,67
itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local.yaml,sha256=l6bQhIt1Yr-1Q0SHS_EXHbF3ZyQUJOSiE6MBNNCX6qc,89
itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml,sha256=WZEot3Q3GrdkS6T4N0p9njfGJGYP8d50rWmRHIVxMrk,105
itp_interface/main/configs/env_settings/no_retrieval.yaml,sha256=lZqV63Sgp9Y6PTolB0P-W9NZ-CrO3LfajyrJBU-CU90,49
itp_interface/main/configs/repo/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/repo/coq_repos.yaml,sha256=cv48hMANb0wM6P_QU6xYCx6uwisSOd6DRtyH-YvoAi4,7408
itp_interface/main/configs/run_settings/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/main/configs/run_settings/default_coq_data_generation_transforms.yaml,sha256=fUpCcPYlyZNgZawPx6Ezjt9seTg-xprZMx6fUsxuzWM,576
itp_interface/main/configs/run_settings/default_isabelle_data_generation_transforms.yaml,sha256=1Tuf-zUn68Hfkv4s0BKr928PuAxtoG66--IZBycjMH8,581
itp_interface/main/configs/run_settings/default_lean4_data_generation_transforms.yaml,sha256=Pn3ZzNhWd3XmZIb3pX9zwVwU99vCTDaTh92oxUDzp8w,580
itp_interface/main/configs/run_settings/default_lean_data_generation_transforms.yaml,sha256=RSdMqP7BDoEJCXzyzyywCIj6kMBFky2Px5g-ecxUfTY,578
itp_interface/pisa/.git,sha256=EkuyvvYn3GZmbU4Id7BUv1sIZJozUec8cDyR1f7E1pQ,53
itp_interface/pisa/.gitignore,sha256=tKu5c7EBxHQ3t7CMownYAuEEcnmWdsWQiAHF5TAMxEs,1373
itp_interface/pisa/.scalafmt.conf,sha256=hM9doZnlR0ApmY_xdMMcaLEMuINdNAVsbhJmUQ_D3bM,43
itp_interface/pisa/LICENSE,sha256=i28B8pLnQZrnoTQXiDedT9ftFaONTMnIeHx5WMgYr4A,1528
itp_interface/pisa/README.md,sha256=B5Gd-_rvNtE3lQAlZrLHYDTYoqorbztaCuQd0JsJsTc,10927
itp_interface/pisa/build.sbt,sha256=8yjmx0ZBwQ0Q0uI_fcwU7sEgJ6LkQmdZuTrp9sSoCC8,2431
itp_interface/pisa/build.sh,sha256=-rxj6w7G4J74MQv7I-pdTid7FlJ-6qgCH4bw7clp9yA,701
itp_interface/pisa/requirements.txt,sha256=j8qh33MtIh84pLd8_9muMo84PS1RK9pxjZ7IKNqwyLo,65
itp_interface/pisa/setup.sh,sha256=a1TeJfct-KReI82OA564fmBYX72iGBwfkS8PrCEbc1o,759
itp_interface/pisa/test.sh,sha256=qYTMbB724JnUpBojK9aznSKMpXI8rwQiOH16UHoYRYU,1223
itp_interface/pisa/universal_test_theorems.tar.gz,sha256=T7LaPjU5_BhkxPLLRwISoAEHenBN8iAlacVJ_tMw0GY,371201
itp_interface/pisa/.idea/.gitignore,sha256=cAA3xsNKKlXb0lHXGkXBgm81LlMI9Nz9HlocDL7tPSk,176
itp_interface/pisa/.idea/ClojureProjectResolveSettings.xml,sha256=lt4OMyhjjaS1MQcITPlKzt_XrHPi5yeRRdCsFj1-Zv0,176
itp_interface/pisa/.idea/misc.xml,sha256=nPeixMTb1ER34QdVq375HXZM8E3ttXN8Ibs8LNiPC-A,328
itp_interface/pisa/.idea/modules.xml,sha256=OxM0OVg-zJ4U-6szachHjVBTD3WY3UC-MoaPD1dNkeU,407
itp_interface/pisa/.idea/other.xml,sha256=26bEN5ObaZ7KIZ0TklPKvmypafDHAiiLOAsE2ff8vZg,186
itp_interface/pisa/.idea/sbt.xml,sha256=pnz0mKxSs9EVa-xkj8MpEVYf0mdqosOuL121WZRQDb4,754
itp_interface/pisa/.idea/scala_compiler.xml,sha256=2lz1ahwvN-hBMZLmI1AbES3Gp8MQAULEu2YRmKVR4P4,207
itp_interface/pisa/.idea/uiDesigner.xml,sha256=jXYZ7D6Dv-hxqZYqLLgWpyfnIrq7DTsSuglgyiPNx4o,8792
itp_interface/pisa/.idea/vcs.xml,sha256=YyPhJkiGKgqW_A14d2coF9bNkeLCo8PXjxCQ2yPG6I4,167
itp_interface/pisa/.idea/codeStyles/Project.xml,sha256=mQI80jGiD1GxH-Fu7VWlAAqqoRGqjPtXTSLhA0_g190,263
itp_interface/pisa/.idea/codeStyles/codeStyleConfig.xml,sha256=ZD-MbVm3MLWxyvxK2FMA7-MCUPLPNHU2JfcU3GVIQXI,149
itp_interface/pisa/.idea/inspectionProfiles/Project_Default.xml,sha256=YK047Tx1EVV6WsoGVcVEYji0SFZnwRB24jV7WuhSMOM,679
itp_interface/pisa/.idea/libraries/sbt__com_google_android_annotations_4_1_1_4_jar.xml,sha256=tavbO8UtkjbYLWeDHDGVwIGxxmnd5vlBAj-574joYKo,707
itp_interface/pisa/.idea/libraries/sbt__com_google_api_grpc_proto_google_common_protos_1_17_0_jar.xml,sha256=cailsfdZDt4pabKRE4TdxU7FWAxTDCB3AMFJqkdBNs0,809
itp_interface/pisa/.idea/libraries/sbt__com_google_code_findbugs_jsr305_3_0_2_jar.xml,sha256=2tLngb5ayV5S-rpx3ZmjBVl5FB4gFAK3Jr0ajOI8riM,682
itp_interface/pisa/.idea/libraries/sbt__com_google_code_gson_gson_2_8_6_jar.xml,sha256=phBxZIer2HNBPX3K0H1r2_Kl1E0VzCUlAinuj4Eaveg,652
itp_interface/pisa/.idea/libraries/sbt__com_google_errorprone_error_prone_annotations_2_3_4_jar.xml,sha256=_JH8VlFujGjPDQzkP7W1ghJyzes6J8EMn_hAFvIFSuQ,789
itp_interface/pisa/.idea/libraries/sbt__com_google_guava_failureaccess_1_0_1_jar.xml,sha256=y52LoXE2ppIQ5bg1SVYcbTvXK96NtVyyD0KL5cxyH6Q,699
itp_interface/pisa/.idea/libraries/sbt__com_google_guava_guava_30_0_jre_jar.xml,sha256=QcWKdNHDYs3tuwwTBAmoL1UO3vjibGMVnrVO-AU0JLA,664
itp_interface/pisa/.idea/libraries/sbt__com_google_guava_listenablefuture_9999_0_empty_to_avoid_conflict_with_guava_jar.xml,sha256=65zf4BfJaAQX5EgWpNykbW_Yko1TNM3it5IJvdTyOmQ,458
itp_interface/pisa/.idea/libraries/sbt__com_google_j2objc_j2objc_annotations_1_3_jar.xml,sha256=ysFs5Zxm662HiEb-Egaiz6FX9vXlXGV8kVVcstL2lkY,724
itp_interface/pisa/.idea/libraries/sbt__com_google_protobuf_protobuf_java_3_12_0_jar.xml,sha256=QBAS5GmTHk3XrFTJDyrK_Yvy3_3GAiTzZc-__uIS4C4,718
itp_interface/pisa/.idea/libraries/sbt__com_google_protobuf_protobuf_java_util_3_12_0_jar.xml,sha256=VlB4eB_JdISvWxS0kNvLKGI8HDOkAZNSoc1xt9Fcbqw,753
itp_interface/pisa/.idea/libraries/sbt__com_lihaoyi_fastparse_2_13_2_3_0_jar.xml,sha256=_C5pjtepsIyfpnZhoehWM4XIYBuLjp_uKySvQaODJZ4,686
itp_interface/pisa/.idea/libraries/sbt__com_lihaoyi_geny_2_13_0_6_0_jar.xml,sha256=xWBaV9QxnMRb8YvoYxPT0wWBj7Ryn3Mn0UrrCDZvD7c,651
itp_interface/pisa/.idea/libraries/sbt__com_lihaoyi_sourcecode_2_13_0_2_1_jar.xml,sha256=wRiwME_x2Xh__zKBEvmQKcgtGjTKzYcWcihjJwnZLiQ,693
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_lenses_2_13_0_10_9_jar.xml,sha256=q3sVd3dC3mVlpSh7N5LChHDnq8wm1mIzY9EihSDOva0,708
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_scalapb_runtime_2_13_0_10_9_jar.xml,sha256=DYrZLAVScAicP058K6kVMX2JDlWEU7o-lG7ZzyF6U_8,771
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_scalapb_runtime_grpc_2_13_0_10_9_jar.xml,sha256=3xZ0s0nTugFCYrIdCRDXDN1YNms1kqybOYRldXDXp6k,806
itp_interface/pisa/.idea/libraries/sbt__com_thesamet_scalapb_zio_grpc_zio_grpc_core_2_13_0_4_2_jar.xml,sha256=mJojWBliZgY6wfaqoxPxNoUpLIF3kYQE_uEh5LZCtKU,786
itp_interface/pisa/.idea/libraries/sbt__com_thoughtworks_paranamer_paranamer_2_8_jar.xml,sha256=d4yOgcoY4aRoQU6zRFsr7f41xJdAW0V6hSuHfB7z5o8,697
itp_interface/pisa/.idea/libraries/sbt__commons_io_commons_io_2_8_0_jar.xml,sha256=uHKRymAiW8KipLydngAiOaBbf_o9FAEScDESclBHfZM,654
itp_interface/pisa/.idea/libraries/sbt__de_unruh_java_patterns_0_1_0_jar.xml,sha256=zy9Dh7MlcIM_lyF28n3T3dJvkE1NeWqiynr3XBbJhLs,667
itp_interface/pisa/.idea/libraries/sbt__de_unruh_scala_isabelle_2_13_master_SNAPSHOT_jar.xml,sha256=P3SsmbtfB_isEAQfAg8k-hMBiF4Q2dBt0fBgbOaxYBE,614
itp_interface/pisa/.idea/libraries/sbt__dev_zio_izumi_reflect_2_13_1_0_0_M9_jar.xml,sha256=_sKMnsHL9Wxa330zb3XDCau6z0MNfOe71CbLEqljYVs,719
itp_interface/pisa/.idea/libraries/sbt__dev_zio_izumi_reflect_thirdparty_boopickle_shaded_2_13_1_0_0_M9_jar.xml,sha256=vmUI2excMaCTpHf0u_0Xl-la1YaEVWkUiVltYjuI_m0,915
itp_interface/pisa/.idea/libraries/sbt__dev_zio_zio_2_13_1_0_3_jar.xml,sha256=t4uhnfC2IbVMnYtD1L8dkte5t22-vG6Lku7BoF8-ZFs,628
itp_interface/pisa/.idea/libraries/sbt__dev_zio_zio_stacktracer_2_13_1_0_3_jar.xml,sha256=gtDHGloQafr3q7VLjjC9-YlLRF1P-Cz4j9wIRdaeNx4,712
itp_interface/pisa/.idea/libraries/sbt__dev_zio_zio_streams_2_13_1_0_3_jar.xml,sha256=ACcZIbQGm6xMal8mKKo9WCdx3jl1mpxBr8AYJ7k91dA,684
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_api_1_34_0_jar.xml,sha256=Bb5mQe6CphxwKTaPuYteAq4At3JH1ofK89gHMi0K1U8,635
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_context_1_34_0_jar.xml,sha256=AVi2yFJXs57fEVqMd---Pn0_GJwPBoMDtqtlXLpnB34,663
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_core_1_34_0_jar.xml,sha256=95ufG9t_25QhUzeoB7QqHaoW96bV3CZjnpsNYahz2QI,642
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_netty_1_34_0_jar.xml,sha256=HqVBHgn9ePCZeopJyk28M7PkVDvkgKOVBF8VEi069OA,649
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_protobuf_1_34_0_jar.xml,sha256=NHaq193cXMgCXO9TwNoYTsDyQkIvVmxy3Lii5FrIESU,670
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_protobuf_lite_1_34_0_jar.xml,sha256=GEgiYKecBet2luVZ52keyh9S4kToI40Hs305_DiXJfU,705
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_services_1_34_0_jar.xml,sha256=GLos04td0XnruOSn-WjaitS6Amby-ARTzwfQhDZ5AB4,670
itp_interface/pisa/.idea/libraries/sbt__io_grpc_grpc_stub_1_34_0_jar.xml,sha256=XJl_cJ12e7SHaq3r3I5ZnDf0HQHTfE5OjezUkQfRI2g,642
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_buffer_4_1_51_Final_jar.xml,sha256=BRMNG3XWdyeDRnOML6KSjYlVw9_M-Sg8z_OpwaAKIVs,709
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_4_1_51_Final_jar.xml,sha256=Kw80IP41W_S5oJ2GqQZK4W5RuxKiChL-qO_DQaKi9A8,702
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_http2_4_1_51_Final_jar.xml,sha256=gwsLg1R99485SLdm1LJgtBsRPw9GqsfGCjwC8L-xp6Q,744
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_http_4_1_51_Final_jar.xml,sha256=Jn1Bc35rBwCiUuekuXdbj6wBJT_hpwMjkstiUltILIU,737
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_codec_socks_4_1_51_Final_jar.xml,sha256=sElPAa2vgZ5Gcf8pETFHtvA0bAvGL5TbkBDzLq_sX-Y,744
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_common_4_1_51_Final_jar.xml,sha256=nwl08cvMwnlnqP3IOgM0CDd1PrEIzv1RpB6mQrwRVcI,709
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_handler_4_1_51_Final_jar.xml,sha256=IMmByehD6zHTv5FznDcbTAWPE0B552WZdjBl8jf1cLw,716
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_handler_proxy_4_1_51_Final_jar.xml,sha256=jHiQvHRD0013sr1eLfSB5W918eOMp7Kv2WSotnw2S6U,758
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_resolver_4_1_51_Final_jar.xml,sha256=iXJv3SyRU_lCmQIKS8DIV8vQF7ZnoVwZiGjl4Ee0cmk,723
itp_interface/pisa/.idea/libraries/sbt__io_netty_netty_transport_4_1_51_Final_jar.xml,sha256=RVxILG_JEYdbmcHfF6aZxab2kcLVgKKbltJfeChmX1I,730
itp_interface/pisa/.idea/libraries/sbt__io_perfmark_perfmark_api_0_19_0_jar.xml,sha256=PJm6LA_y1h7O_XpAzyxOwMfNIX7jbvb_BhH1f-TcE8s,679
itp_interface/pisa/.idea/libraries/sbt__net_java_dev_jna_jna_5_3_1_jar.xml,sha256=YoJmpTVHrVUWCwEmaZyRyWaO2cn-BQb81N2MJxBfsIQ,629
itp_interface/pisa/.idea/libraries/sbt__net_liftweb_lift_json_2_13_3_4_3_jar.xml,sha256=wqdrSPWlaLRFCsbtGb39jW94GD3-GmislOkA_72qHRw,686
itp_interface/pisa/.idea/libraries/sbt__org_apache_commons_commons_lang3_3_11_jar.xml,sha256=ZddgisfkMtIaoUrVqGPFrdeGSPwOQNvoYoG0ZoazC98,700
itp_interface/pisa/.idea/libraries/sbt__org_apache_commons_commons_text_1_9_jar.xml,sha256=d5hxaTEnPx5FakO34_IfGg_W0-H_0X2G5s5uGT0j8eY,686
itp_interface/pisa/.idea/libraries/sbt__org_checkerframework_checker_qual_3_5_0_jar.xml,sha256=s3KAgcQETsUi9zhKhsLlkZe_ZQzy5-5t2SMSQr18Nsg,708
itp_interface/pisa/.idea/libraries/sbt__org_codehaus_mojo_animal_sniffer_annotations_1_18_jar.xml,sha256=3WXQYTl5XgKDXNgm2OFhojxRsZlvPCIvsagY1estzYU,787
itp_interface/pisa/.idea/libraries/sbt__org_jetbrains_annotations_20_1_0_jar.xml,sha256=NX0ViQG7oI4LpMYCSBunYXLVLD6NcBqM_SjpErDK8P8,680
itp_interface/pisa/.idea/libraries/sbt__org_jline_jline_3_16_0_jar.xml,sha256=piGWasIla6jWNp73-4znDimWWlh-36D6Zj4kLlaoda8,622
itp_interface/pisa/.idea/libraries/sbt__org_log4s_log4s_2_13_1_9_0_jar.xml,sha256=381FeZdX33l8AaMYXhXoJT5HIi93ES7fW3Az2WqKGhg,650
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_modules_scala_collection_compat_2_13_2_1_6_jar.xml,sha256=qWU6j1tHGkYNdt3GNajLkydy9AGJoMGvX-83Xby0WBM,828
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_modules_scala_xml_2_13_1_3_0_jar.xml,sha256=0jK4S6xgWGXS_rE3IoN5P8JFcmUI-Ev0x1iEYV-3xeg,730
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scala_compiler_2_13_4_jar.xml,sha256=eaFdJ_UGJlXFV5ZtN7uR0r10Q6hsdVRX7W1YxIliZqQ,705
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scala_library_2_13_4_jar.xml,sha256=Ga1Sqvle3aRBMe-aUd0-HRwnk50WkxcPgSmvsw9b1k0,1607
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scala_reflect_2_13_4_jar.xml,sha256=q2DFZa1zh9mOJRQ49T3zauIY-d73TVYt2cv26dSnSVs,698
itp_interface/pisa/.idea/libraries/sbt__org_scala_lang_scalap_2_13_4_jar.xml,sha256=o7QAwq_Gg3AhU9AIqtnZe18Ek6oPxWA02LfMap9n714,649
itp_interface/pisa/.idea/libraries/sbt__org_scalaz_scalaz_core_2_13_7_3_2_jar.xml,sha256=iHZ_-DBwgAa59Fry-e3WF3xK4tDio1QbbbWrdi3tj6w,696
itp_interface/pisa/.idea/libraries/sbt__org_slf4j_slf4j_api_1_7_30_jar.xml,sha256=zGE03ofrEOhfCR4taecy2q41bcf6BEN_7S6Ww8hYcgQ,650
itp_interface/pisa/.idea/libraries/sbt__org_slf4j_slf4j_simple_1_7_30_jar.xml,sha256=NV4R-ak6x0CWCRHddZwZ0E3Em5u7Letu_z9AhcKvnYQ,671
itp_interface/pisa/.idea/modules/PISA-build.iml,sha256=p0U_Gls2ItZTFnnVY-3wGtSLyTUFaNiJ-ki2uMpkozA,14533
itp_interface/pisa/.idea/modules/PISA.iml,sha256=yIxJ7NDIQTMz5etQvp-HqBkGs-QBYAcgFyOCr7yqhwM,8415
itp_interface/pisa/command_generation/close_gaps.py,sha256=59dc6YhJrMpfrqWE7Bxi49OgncWd2jignGMH4hIbLeg,1379
itp_interface/pisa/command_generation/conjecture_normal_order.py,sha256=5XeeERBTvvAAMzhQLsnqvVSwg3MFTIa7LzEG0ighDYw,3060
itp_interface/pisa/command_generation/conjecturer_command_generator.py,sha256=pJnhn_9yErWMjURRd5qee1zZcVAGpqMYEdd7NHyC-Sk,1761
itp_interface/pisa/command_generation/create_dirs.py,sha256=wgUzEZQIQEeRO2pHMiys6ITsxAqr6GhVc8--aOsKRhs,384
itp_interface/pisa/command_generation/find_std.py,sha256=YHGPP1Hgo6VAckKLIeCIb7Y3IS3Fd2gsgXPIdU30KyM,3726
itp_interface/pisa/command_generation/generate_build_commands_afp.py,sha256=VGBZu177uiRJdabuF8yNWGMCLkuM8LKS3or-PGeTsUc,480
itp_interface/pisa/command_generation/generate_build_commands_std.py,sha256=oFhvrm0K28Ju0xplu2Z-kakhhl8C4WgmEOXPUdIaj1w,517
itp_interface/pisa/command_generation/generate_commands_afp.py,sha256=iQADP4ITDsh5oUYvHxExBxPv8SYiCM8jirdtMXsD_3s,4113
itp_interface/pisa/command_generation/generate_commands_mini.py,sha256=XwkBiI6Knm1MZnoLWIBGC8EXHVg4TP3FMNUPYzHfDCc,3250
itp_interface/pisa/command_generation/generate_commands_std.py,sha256=njhvBxLWU31AHfhOggPIjvrjDmwTuuxyTzg4cyNKVJo,3012
itp_interface/pisa/command_generation/generate_hammer_extraction_text.py,sha256=MnMqsc4KZaQpdwYA3DV8V2BM64Wm-haO8Ia8V_aQcgo,223
itp_interface/pisa/command_generation/hammer_command_generator.py,sha256=77WhleXSAuSGhHDV18DQ8u7uupgxBYhm-sPWExGc3Og,1944
itp_interface/pisa/command_generation/hp_search_command_generator.py,sha256=0P5MUO2UA0WV92F38dEcEHEMwaqRZF4M_5FiikhTasY,3561
itp_interface/pisa/command_generation/oracle_command_generator.py,sha256=R98GKb4bg5h27o4dUsifiTCawFUA44UcqvE1MiQbQos,2435
itp_interface/pisa/command_generation/search_command_generator.py,sha256=uc2Fu1Sz1_ML1GbhTSNLg3vQvBWe_IcZBJySnE3rMkI,3535
itp_interface/pisa/command_generation/summarise_problem_names.py,sha256=Zrln1GehwsxytX_PduBADB_6SeaR07bmNQEitF-gShw,1792
itp_interface/pisa/command_generation/tpu_hp_search.py,sha256=he8MLw5YzKFmsu2glEa-ZCE5mU4fNHVvYv8To2bnOSU,4232
itp_interface/pisa/docker/Dockerfile,sha256=2iJ5uyTf7y_0nmRK4gpMi_Hl0WshpSUMtLEQNfEzURc,1059
itp_interface/pisa/docker/docker_tutorial.md,sha256=c3tWzEa-hHIovQbOPiYYqaYUZ20WTnXdz7omnitVNoU,3172
itp_interface/pisa/eval_setup/copy_isabelle.py,sha256=UScqTAoTLoo1d8ZL6oR-APa7qW4goEbfdrFV0D33GHs,1845
itp_interface/pisa/eval_setup/copy_pisa_jars.py,sha256=KSiqDGygm_yob4c55m7ErXbNt5BPI0lI69MxgMoU66E,548
itp_interface/pisa/mesh_transformer_utils/tokenization.py,sha256=jgFOhfQSL-I2TTzj8WRj0DqFBVMcfLTYQHVSIKlcGNs,2271
itp_interface/pisa/project/build.properties,sha256=bT0BCGnSmlL_jBkYUlMmEuLBjlCP8GeFDJu5OhslQjA,17
itp_interface/pisa/project/plugins.sbt,sha256=lkwcz9ot4vSvJ55_qqh2Y2peCRJcX2PsIeiNcPNEsKM,238
itp_interface/pisa/scripts/extract_last_k_steps.py,sha256=b4anmpE95GG8qbDSCfsTY79ktMoDSGEr2u4jiWmWfvQ,1350
itp_interface/pisa/scripts/extract_proof_corpus.py,sha256=3-_3HH8rcFfmGXwoPAHOT5smoONnKz4qHJMMgWbwSJs,655
itp_interface/pisa/scripts/gather_hammer_results.py,sha256=yag_crWGBpIlmu9y9B2SKok_YJFw0Lh88WfU-yN9qqY,1133
itp_interface/pisa/scripts/length_in_char_stats.py,sha256=vnirnbkeWKjzv1UJ046iAZBWXnJKwrE9KffwZOHNfgs,815
itp_interface/pisa/scripts/mix.py,sha256=uq2WZEZwGdNqX_4swTr77Z5wn0U1K0VRVg8hFCAtCzQ,5133
itp_interface/pisa/scripts/results_stat.py,sha256=LS4c3oU5tHcJJVr9F2tZlXj43WE3tNYxkR-uz5GeMb8,1629
itp_interface/pisa/scripts/test_array_job.sh,sha256=5RW5w5OHwrQMUeyZU5s59A77TduahDo285efHvqgejA,1268
itp_interface/pisa/src/main/protobuf/server.proto,sha256=Rhts0ExxT6V3HNhXGvvy6vzPhP89ZVY2epYy_7DExtI,1526
itp_interface/pisa/src/main/python/pisa_client.py,sha256=dhE8PLAvENYSGGg8IkRIJCmpwj2vslS0od4cLPrDbCw,13866
itp_interface/pisa/src/main/python/server_pb2.py,sha256=a4BjfiwW4qGUUBUxZYGwrQOmT2PaQa62Az_EBHcKR8k,12704
itp_interface/pisa/src/main/python/server_pb2_grpc.py,sha256=hYu81g5JNmqTpOqTXee8TjosWtHwsmWlL9cgXPF5Hk0,10076
itp_interface/pisa/src/main/python/test_client.py,sha256=qC_s6HiV_fYGjGQISqN07jQm4tmn9wd_wOUU_Nfo4Ss,582
itp_interface/pisa/src/main/python/test_client2.py,sha256=R65RF5YBaoKpq_zxR1NPTILXHssoT0DNMtWrDBS44EY,2640
itp_interface/pisa/src/main/python/.idea/.gitignore,sha256=cAA3xsNKKlXb0lHXGkXBgm81LlMI9Nz9HlocDL7tPSk,176
itp_interface/pisa/src/main/python/.idea/misc.xml,sha256=WdkfFrZjLX4rXiDJ-01dO4gM-6zMut9OmKVddZ14JDo,278
itp_interface/pisa/src/main/python/.idea/modules.xml,sha256=qBvl8A1uBtIAvIFsJtAXz_ifRc9Qz7YvlHUPBqvB06s,264
itp_interface/pisa/src/main/python/.idea/python.iml,sha256=w0TW3o9qEaYr1iYR1jwYqlUBYm3KyxgnCK1PD03XvwQ,441
itp_interface/pisa/src/main/python/.idea/vcs.xml,sha256=ZEt22h_UABai6qzUWvAjkIdEIg4UUHoZBGut3J8go2M,189
itp_interface/pisa/src/main/python/.idea/inspectionProfiles/Project_Default.xml,sha256=0DOYP9n5RgCCFXLMl3jEQdSdLGyEdPAldPzyXg9IzFQ,743
itp_interface/pisa/src/main/python/.idea/inspectionProfiles/profiles_settings.xml,sha256=YXLFmX7rPNGcnKK1uX1uKYPN0fpgskYNe7t0BV7cqkY,174
itp_interface/pisa/src/main/python/conjecturing_parsing/conjecturer_postprocessing.py,sha256=sd-QF5boU6Bavk5PmXL4XmlhE0YZ929yb1h3qSg7mrM,2562
itp_interface/pisa/src/main/python/data_extraction/extract_data.py,sha256=Bqv3bP987ukDtqJVo9EB3wufOX3kF0P0jfLZAgq9Ef4,6623
itp_interface/pisa/src/main/python/data_extraction/find_premises.py,sha256=LIUl7WsaYavHc5XZBpqpsrdZBrwMyRjVe9dmANN1L8o,8686
itp_interface/pisa/src/main/python/data_extraction/process_data.py,sha256=UUYA4FU7PRBd6vSvLS5_FcxerSuOjeUEP50IK69l4mI,4890
itp_interface/pisa/src/main/python/legacy/PisaFlexibleClient.py,sha256=pfxIpjU2qMnaid8oGF729QyPkrIuVqbW1KoFa739MK4,6456
itp_interface/pisa/src/main/python/legacy/autof_test.py,sha256=Pw8N3LoJM9CVKoAreHXvRzWyWgBbwITbLnwfYvkgvQk,2181
itp_interface/pisa/src/main/python/legacy/cmd_client.py,sha256=_F47R0PDmzRNc5NaZ7X7t5cXzBs5Rk5KjQTOIv5RwtU,1029
itp_interface/pisa/src/main/python/legacy/convert_scala_dump_to_test_name_jsons.py,sha256=UcAiAftM4btdXDzCCun-ljhkJCn4sYLs0J4sCCZFZBo,667
itp_interface/pisa/src/main/python/legacy/create_data_txt.py,sha256=oIRswEuzbkd10MSRN9C4GYNLrlIqKQ2JfM0siYQKJxU,3430
itp_interface/pisa/src/main/python/legacy/create_finetune_tfrecords.py,sha256=CYMpL9381lpT7BZDX-oOhSZ4Xu16rSBPum3SnGfeDFw,11844
itp_interface/pisa/src/main/python/legacy/demo.py,sha256=6MHJn-S8yll40GaFkCqIN8HQeMEmun0WIxEmhQF9wrA,1731
itp_interface/pisa/src/main/python/legacy/evaluate.py,sha256=KwXLXsb5oXz3fWfwGC9SqV20h3y1CoIzbLILymqIxIs,5085
itp_interface/pisa/src/main/python/legacy/extract_first_step.py,sha256=-NGbtQguEhDdnG2ziB8FEUDm0FwWyGLsyzqyE6O-d-4,972
itp_interface/pisa/src/main/python/legacy/get_global_facts.py,sha256=sRQP7qD8pH9LkUPqVgI5nXzG0kPadgJTxbVha-4Tito,1405
itp_interface/pisa/src/main/python/legacy/mix_data.py,sha256=HHaaAfrYXesxNe8S91J0-rn7lE375GVZymHFcvS8cYo,964
itp_interface/pisa/src/main/python/legacy/one_stage_extraction.py,sha256=9FAVpkGzvGGoysk34nq8i6nvp5hbFE7Aia_3i0jizF0,4741
itp_interface/pisa/src/main/python/legacy/prepare_episodic_transitions.py,sha256=hbRXG0SVyWtuUteSi-pNx9NxzVdFLkFPXmapm-VkH_4,4612
itp_interface/pisa/src/main/python/legacy/prepare_translation_pairs.py,sha256=3L3txoUBF4o-PtnzIb-JlUM9Dl3DvWwA5yCu8jSmuXE,11168
itp_interface/pisa/src/main/python/utils/filters.py,sha256=-owsWZ8rNQuvQN0LRn9SNDvzYP30Cv30ujqh_881zBU,2575
itp_interface/pisa/src/main/python/utils/pisa_server_control.py,sha256=_gSQDDTbY15ulqjnv0RVx4WRAboyFWV6vEChDAcrvkk,922
itp_interface/pisa/src/main/scala/pisa/agent/CheckSyntax.scala,sha256=JYb8lppks_ismh-lQd3ytz-qT1HhCsYjAZPiqCLwDdI,10217
itp_interface/pisa/src/main/scala/pisa/agent/DepThms.scala,sha256=L8WQcLKXW3_o9J_-3J_p2q6GT7CDG6lwprB36YekTec,1034
itp_interface/pisa/src/main/scala/pisa/agent/PisaStat.scala,sha256=Yh64Fukl6UOIvu8F5_Pvj9pZVxV_XTPc_KptetSNb6g,1726
itp_interface/pisa/src/main/scala/pisa/agent/RefactorTest.scala,sha256=6W20rHLqDMvQo24kSfvLQMwRPnNfnBEzXjGUjN1MAnQ,1996
itp_interface/pisa/src/main/scala/pisa/agent/RepHammer.scala,sha256=oYYvplZPNA94QzkzztwcqJEDjPzp8lYyxTlmw1xjyzM,4500
itp_interface/pisa/src/main/scala/pisa/server/HammFacts.scala,sha256=uii2djDfIJMK_Y04hKpWe2g5A4Bn5SKp4JlXEqjJGzQ,2808
itp_interface/pisa/src/main/scala/pisa/server/PisaOS.scala,sha256=Wc30bWItiPgC3_QkpOtv_VQZDlHUIPRMsbipfTLLt1M,32964
itp_interface/pisa/src/main/scala/pisa/server/PisaOneStage.scala,sha256=YbhxKql-205yFUniCJ33NxISNrwkXZaYjW1gqlryngg,21885
itp_interface/pisa/src/main/scala/pisa/server/PisaOneStageServers.scala,sha256=yJeRpzq7fnHyVcfB6iulrq1_R6xyG80YcoYAhA3E6B8,33535
itp_interface/pisa/src/main/scala/pisa/utils/TheoryManager.scala,sha256=GwfzLfQuEbSdYJ5UxCq_0GGS0RPSWN_bD7rpmhyzWCk,4529
itp_interface/pisa/src/test/python/analyse_debug.py,sha256=IrqK0zjuJVI16zIcPrWBP8Bhq3qv0N7-FBe_uCcu-zI,1568
itp_interface/pisa/src/test/python/extract_test_seq2seq.py,sha256=xAPTL8j3-y4B2J63zkSsWtUTmxn7_1r7ojy1IwRreQ0,1753
itp_interface/pisa/src/test/python/extract_test_theorem_ground_truth_indices.py,sha256=vdiD5KnBZVQxxHG3W645SgX2oOTrTt5W07CNPDo7iDs,1154
itp_interface/pisa/src/test/python/proof_originality.py,sha256=fjZNKj3WFDWJNNqOAPXEV_CBPulUPXFPgzl4ZIbr71g,854
itp_interface/pisa/src/test/python/test_command_generator.py,sha256=sgPJPf5aWeB24y-L4svP7WT2m69sJJyIBuvVQXoOGW0,926
itp_interface/pisa/src/test/python/test_model_sequence_accuracy.py,sha256=O0duQt75tDuxN5OS8I5SpwLKEYvcf2edL1IA_Sfhrko,2420
itp_interface/pisa/src/test/scala/pisa/Easy.scala,sha256=8ft5vOqRn5nt64ZXZxcp9vLjaNxJl07udk684Y2vCzM,851
itp_interface/pisa/src/test/scala/pisa/TestCurl.scala,sha256=3u-5y_3rpPqa-8XAy_lfRLGnUEPzIZv8xejArcPhyeM,2819
itp_interface/pisa/src/test/scala/pisa/TestIsa.scala,sha256=6vH4B5Lt5P7xo_XNhRp2A7h1ggvjN4RBAmgC89F_Ev8,584
itp_interface/repo/build.py,sha256=taNMSja1OTGSnVZmRJt_AdGxRAFTYR1psrs_YC0VXVs,2985
itp_interface/repo/clone.py,sha256=ytQEt0jsz5K9C-LgnZ5tr7kFENAzcEjse5w5QsdUrvY,3256
itp_interface/repo/dataset_discovery.py,sha256=DMiUxynMYdi4w58faM0ns1G23hSKr6NivCz2OOyoFF8,3819
itp_interface/retrieval/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/retrieval/abstraction.py,sha256=5jbbZelSdccmJ6AzYuD936xnr_yFSwG2FRPcrZCaR0U,733
itp_interface/retrieval/coq_bm25_reranker.py,sha256=pgfL_HSquYWh81-6Ft_3VSMH3pitBKRLD513D9uaRR4,7213
itp_interface/retrieval/isabelle_bm25_reranker.py,sha256=_y9zasFxnjLP5wIPBn6HUSG2Tmrc787FuFjfMXM7LPY,3595
itp_interface/retrieval/lean3_bm25_reranker.py,sha256=F4L-LT6MDm9fIFphayFYJThQdz8w-4WIN_v9dnv-tzQ,3788
itp_interface/rl/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/rl/abstraction.py,sha256=6n2Mv7ZzCPC50lN85CWH_G5Wa0V-c1YW69MVPwa1JEQ,3236
itp_interface/rl/proof_action.py,sha256=BwFIbeoGQOT1R1SRNrXPfB7sS_Wq_vkhv1XOLgVnzaQ,7490
itp_interface/rl/proof_state.py,sha256=B8hkBhdhg6RhK141JpeWp48skTZiAQwvMfpxOrbhr90,8468
itp_interface/rl/proof_tree.py,sha256=cutNP29l5Pd6KTtor03jDz3JXRQ7dWckzKCt0N_HFPo,4116
itp_interface/rl/ray_proof_env_pool.py,sha256=MtcM4Ur-mQNwYpjX6SWOtmJD31TBsPTygULBLWJ8Ys4,24906
itp_interface/rl/simpl_proof_env_pool.py,sha256=g2WX7OOv8Cow8t12CVjN8GwIgYtuCAGPoGFdYxvw0oc,792
itp_interface/rl/simple_proof_env.py,sha256=F0IEBsY6IMBYiV5Rsz_up92jVjzSn4M_x90wTU7GYeo,38574
itp_interface/rl/simple_proof_env_pool.py,sha256=kxwD4lMEbTzqQd_XG_Yrs19xRB5TtQo2SgyykdX0wGs,4386
itp_interface/rl/simple_proof_env_ray.py,sha256=NUMpMbc1prCvN24eiL5_aPEJE9s5sIr5A_MXcOmsp7E,3104
itp_interface/rl/thread_proof_env_pool.py,sha256=LzTvPifHz3QPHUCuuegFMClmq2ZeQIjZiLLVsI2nX5s,22601
itp_interface/scripts/setup.sh,sha256=DxP_JbHhNUiHwZBeLv5bIjfUbxGagB8rJhezaOO-nAM,8088
itp_interface/tools/__init__.py,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/tools/basic_utils.py,sha256=yQxzQhfdmyrRKIZKwUYROACtSyk1ANUwJxB-acq_7Z0,6344
itp_interface/tools/bin_packing.py,sha256=3XSo-bmEDSI40g3aK-lW4BhYfJX5NtatgnA2Wu-TV4c,3827
itp_interface/tools/cache.py,sha256=G-R4Cx5XiC3t2SzaPLDeXkWPLsoJOo6bbdHotRyJAYU,3018
itp_interface/tools/coq_build_spec.py,sha256=H_lehkWG0t8tLuJesm99AI49n6gp70MjyxqvmopPdA0,1081
itp_interface/tools/coq_context_helper.py,sha256=kR4A7sMQ1OnflOmhpRARM_NTN3j6NwP0_lW7ZpQ9fCE,23145
itp_interface/tools/coq_executor.py,sha256=mQJ8MX2g1raUgAlKkorCD6KqhHJRBgE2AHOekZkmUv8,21641
itp_interface/tools/coq_local_data_generation_transform.py,sha256=CSetyT7N-q9lpXf4IQGpFP1vYgzPKRbk5-MuylsVTuw,9045
itp_interface/tools/coq_parse_utils.py,sha256=PGtaNuF-M6iZigcIbsRGOvNQiMxV90NhhET4oYYso8w,6483
itp_interface/tools/coq_theorem_proof_pair_generation_transform.py,sha256=cpBGLVUdSr1tGVdcDNdvYD9NbO23zWAwtI2s_9r9XFo,8354
itp_interface/tools/coq_training_data_generator.py,sha256=wJ3ODVV-ZWwABYGnnitvDMgoSoQ7p-HBdiD0SVjZvww,2702
itp_interface/tools/dynamic_coq_proof_exec.py,sha256=PCj8vI5oitsAynp8-9r93c27Z7FAVqF50ZdX_IZXVsk,11202
itp_interface/tools/dynamic_isabelle_proof_exec.py,sha256=XsiAzyWl4CwWGBU5zH9Z3ftiyy9qerJ0JqgHJzwVqXQ,11834
itp_interface/tools/dynamic_lean4_proof_exec.py,sha256=5Cd0-_cXwRT8oN9a1i3rHQZ8WcHpOu19X-n8HMKIbPw,10640
itp_interface/tools/dynamic_lean_proof_exec.py,sha256=mlqxdHnCYeA-NeU9_BmzjYPXwF2j5lU4IEMS0eXpVz4,11744
itp_interface/tools/isabelle_context_helper.py,sha256=tFzO2pcQt458BD1uwWJja_jpu_yjGDOEP12d_vgfl4Y,4175
itp_interface/tools/isabelle_executor.py,sha256=g6wir1Hzn0lbcHIlA-G0MhaaFGbzNXTewusP5B6l9mw,38369
itp_interface/tools/isabelle_local_data_generation_transform.py,sha256=BgIjuQu32P_PQsb1pLeMu2YwkUh0R9UKVrTkaH0a_88,8426
itp_interface/tools/isabelle_parse_utils.py,sha256=wzEc1NxVtjxywyvX61bDQ1uYOD33Ubgvzblby_ScL-Y,4932
itp_interface/tools/isabelle_server.py,sha256=rgmaiJL2oEUMHgaYMBPMqiSIhoFlndKYszjBzA9VP3w,4168
itp_interface/tools/iter_helpers.py,sha256=Z8eIZOHfxLGYRdzahW0XF5ansFoQ1y4IrVu7yT6eY_E,2318
itp_interface/tools/lean4_context_helper.py,sha256=kVruq38YKlWf5j_SIhOatYH2pTUn8LSms-_p_2Hs0bQ,4532
itp_interface/tools/lean4_local_data_generation_transform.py,sha256=2blQQhWbHXjKgUIV73Sc_5IpxrX7IXaPq8oNJNWFVsY,6323
itp_interface/tools/lean4_sync_executor.py,sha256=ZVAtGFZDON_jijU7gul__GAqQ1K-SWbwC7Kuu4FfJpI,70259
itp_interface/tools/lean_cmd_executor.py,sha256=P22SAi3WyxmlChyzbfMBueXDln-IUsKKhL2xBaXsdKQ,37949
itp_interface/tools/lean_context_helper.py,sha256=8KzSHLjgsWxtaSUtXL_sg3u_Cmh1wjAf9zQsNdX6soE,22006
itp_interface/tools/lean_dojo_data_generation_transform.py,sha256=oRuKShG9TXYNtxz2Ny89fzX57sZcUe-h3x3cTrp4YYA,11282
itp_interface/tools/lean_executor.py,sha256=grEJinlb_hT4q9bbJCZlHiiNDLyT-oeg-NyVVLaeG58,32209
itp_interface/tools/lean_local_data_generation_transform.py,sha256=qW80IxZFptqWptd0eqWve9nrNFTNxHO2uhGTFP9iJik,7796
itp_interface/tools/lean_parse_utils.py,sha256=srrZti-2BCeiECdTXu8wwU3FgcdzMcM1UKir3GJbuTk,2276
itp_interface/tools/log_utils.py,sha256=SygDUvTlZLUxxeiA-4p1kpGy7YB7gIkOQuN7gWi4xHw,562
itp_interface/tools/misc_defns.py,sha256=Wo4lhNYpqGgYYs0uQ9V9arqCC4hoD0PgtZqqJRD46PA,384
itp_interface/tools/proof_env_utils.py,sha256=PvlQBUbJ-wr5Jx6KKrsx8hjQsPqU84o617gAhUK0K3o,1018
itp_interface/tools/proof_exec_callback.py,sha256=H6gaSEZqD1Ihz8-tnUxoGCUp5H-lrwUtSkVQDbmKuIs,6944
itp_interface/tools/ray_utils.py,sha256=wJC9XohYoaT2aXCYZmRQIuBDT1WNvMNOA6U8ZZOwT6w,10825
itp_interface/tools/run_data_generation_transforms.py,sha256=EYa6byqJs9ymxMoFV-e0iALVUcD3NKVaJUnsjOh3x_c,27492
itp_interface/tools/simple_sqlite.py,sha256=Y7yS_x1K2hWylglCSWdv6XWN4HaR58-TmQ-kBHMueTg,29831
itp_interface/tools/theorem_details.py,sha256=Aeied3x0q3cMgDpnYYJiQJdsskYiD0HfCZg-X-oNmB4,830
itp_interface/tools/thread_resource_pool.py,sha256=BQcX5fcoSFr3oG0m_5ENthQ9RL8nfrVpYLxzRN_IN8k,2514
itp_interface/tools/training_data.py,sha256=OuNz-zNgJV5LXBvKKad6JRYhVw-rLpgFMEqS2I9mWME,29447
itp_interface/tools/training_data_format.py,sha256=xccfvCcATXKa6UWLXOVNDP89A7S5yetacErdTM7kCCA,39748
itp_interface/tools/repl/.git,sha256=JsACm7wvQdCbsjejV8i2GEYv1KOga4kc3LHkKu6-gyw,62
itp_interface/tools/repl/.gitignore,sha256=osgR5UUW7jYu360uigGI_CYKp7hCPs8jQmfIOzkDu_k,120
itp_interface/tools/repl/README.md,sha256=M3Ece6O_UYIJeCEt5h1LjYhZ6KLhxB_8f0Vwi1Y4OJY,5286
itp_interface/tools/repl/REPL.lean,sha256=uEPB67EZJSLzpkrKSzIWjdvTZbMKGRRTilO6AQql2VQ,81
itp_interface/tools/repl/Test.lean,sha256=Gc5tYTk1JzIvGmGHbHXQok3khpUPE40JXiNydSxkjbI,254
itp_interface/tools/repl/lake-manifest.json,sha256=dPMokVDfCv_EtT64kR482hqGVUdS4PMfsg6NDFHHYy8,110
itp_interface/tools/repl/lakefile.toml,sha256=aoAZM0R1PtidPxB1QOHlz9YspDWtK7Et_vFEUP2YA5U,183
itp_interface/tools/repl/lean-toolchain,sha256=0k_tQ007E636q1dySgp_Jw6ovxyBi1rlzyXLziTdaFw,25
itp_interface/tools/repl/test.sh,sha256=hGpGQoND3n7DAqXZyBL_hEr_DA0S52fKHYucbFs4OaY,1229
itp_interface/tools/repl/.github/workflows/ci.yml,sha256=nin6_28PeDneH4B_IVeJD-uDO8H7mbUjrtETiyA_1Z4,526
itp_interface/tools/repl/.vscode/copyright.code-snippets,sha256=Yxvq5EWxIBkQzq93t7Iwyu9L9c08LHz_AZE1CUMLWWE,273
itp_interface/tools/repl/.vscode/extensions.json,sha256=kQeb1JmqB4cCDbyakYNnXDfMuQmUJgMiBBmGQj_sZ8M,485
itp_interface/tools/repl/.vscode/module-docstring.code-snippets,sha256=3bRL7E2bsmcq5SkkNy_oMWFakjqq4BjE28l9meCQ4gM,536
itp_interface/tools/repl/.vscode/settings.json,sha256=OlcKRIcoVQKN361xK3iffrfdtuos4Kyxo98R2xxrEIo,301
itp_interface/tools/repl/REPL/Frontend.lean,sha256=BC_kcJ9Lo73SprIYq2bLsj7G5FbNBWIZec6hjCASBQ0,2360
itp_interface/tools/repl/REPL/JSON.lean,sha256=h1VNu5FQQ7pr6mOAcVQi5us-sLjP1bR-Ma1Jrti06Us,5023
itp_interface/tools/repl/REPL/Main.lean,sha256=AbWLCfqkfDFta0DBYXLVLQaYM_igYQumQyQezD1FFPU,16992
itp_interface/tools/repl/REPL/Snapshots.lean,sha256=EH36ia4sU8_08zv8A52WI3oy1XqRuukku7u8OvdPyac,12169
itp_interface/tools/repl/REPL/Lean/ContextInfo.lean,sha256=frgYburPj69mkNzZY2riBUc0Pdx7NoPssxPhbtZD184,306
itp_interface/tools/repl/REPL/Lean/Environment.lean,sha256=-cbonTFGufQgd5u6JB5BzGFK6v_WbOPt8ipbHQMaTxs,932
itp_interface/tools/repl/REPL/Lean/InfoTree.lean,sha256=yncOdTfSr09nw8cH63beTJ6kEPZUhkQEo4uhW7vKoYM,12494
itp_interface/tools/repl/REPL/Lean/InfoTree/ToJson.lean,sha256=GyZtO-3quowiayeDtwDkXZPGtLi0QsV37MOSzUk-mso,3722
itp_interface/tools/repl/REPL/Util/Path.lean,sha256=TvKRqMG3Y-HuV1DUbc1rxvm-WonGqfe1d4FK1hGTsWE,1216
itp_interface/tools/repl/REPL/Util/Pickle.lean,sha256=fUulkI1e46F6qda7emBjUpt8bBeaWqkHQ7oG59Tu-VU,1578
itp_interface/tools/repl/test/all_tactics.expected.out,sha256=LUnPPQwAViJ72DHhU40-cwBcsskwbzynpSuG_pC1xYY,423
itp_interface/tools/repl/test/all_tactics.in,sha256=ij6NPBNKHY-xNy6Nr-xv5aPVMLORpO7U63k6Zsgh3kY,71
itp_interface/tools/repl/test/app_type_mismatch.expected.out,sha256=4aYdID-AS4aIE8g48mlIzepT79yKz8fgNbOzjjcl7f8,851
itp_interface/tools/repl/test/app_type_mismatch.in,sha256=2uCSpI5axnbTP1syUocYjuFIuAQ8BVxknxn-dtchkQI,224
itp_interface/tools/repl/test/app_type_mismatch2.expected.out,sha256=rZaJOZmRrU8rjLKVK9zoTn_0LqIKW6uinOnF-uFUoW4,1772
itp_interface/tools/repl/test/app_type_mismatch2.in,sha256=C2NMH5jQvyLKoxseaMBxghmXY4PiaoWe-AKjXnGa7VI,390
itp_interface/tools/repl/test/assumption_proof.expected.out,sha256=ZSyFK3laOmXS6XKnbo5FefU-VxVgUmK9sJ92FN3rGe8,384
itp_interface/tools/repl/test/assumption_proof.in,sha256=hlMhL8UUpb-AGLT5e4yHM49d1hPDIyYQE0v04JxXkb8,109
itp_interface/tools/repl/test/by_cases.expected.out,sha256=XwQczJl8vBqPpWnByk9LnrQLzaWG4OnI6aAsW8E90R0,846
itp_interface/tools/repl/test/by_cases.in,sha256=qScl0aS0yBDKxpOD9WhBt5PWW9AQz3d6LQgSLgyOJyE,204
itp_interface/tools/repl/test/by_cases.lean,sha256=3g-tTWDLYZFmoaTdiYhNam1BajLUcSp_0ptMzGuDnhw,85
itp_interface/tools/repl/test/calc.expected.out,sha256=q9qzJdfgDOQzUmUuxsdsrzlji26K8SFna0wSUf2sdc4,1755
itp_interface/tools/repl/test/calc.in,sha256=xQDQTyYYybHeiWNyIsML8acWHA53fzxnSxgTgo4dOr4,101
itp_interface/tools/repl/test/def_eval.expected.out,sha256=oT6oYHCQJWQJrSIDjFJehXl6aYrvW4F3I2cN5438Wl0,163
itp_interface/tools/repl/test/def_eval.in,sha256=zBBJKJ7p1yKF0SHNIJ8MROW3XN5NNCVpTnO4K8pQZqc,67
itp_interface/tools/repl/test/dup_msg.expected.out,sha256=VbI6-LQV23eMpUaTVw3lcQNBt1YhDzNvq-R_IRSCLbk,322
itp_interface/tools/repl/test/dup_msg.in,sha256=L4hJbuydhf4BEe6i8oqDatD_f0WbnQ4yZKDcJrtnYmk,84
itp_interface/tools/repl/test/dup_sorries.expected.out,sha256=Uxr31SbMowG_oo6I1kMAujGxCgl0dtXRcIU5PUnJfgM,606
itp_interface/tools/repl/test/dup_sorries.in,sha256=HHfFCl9ig_Q8IUSsW1EC5UgTxKUZip_TsoeQKW7i0Vk,93
itp_interface/tools/repl/test/file.expected.out,sha256=k5B3RQs15iRkeMqgOtqidJWpVXLklnfknd8sKtmOn64,267
itp_interface/tools/repl/test/file.in,sha256=yED0oLwIcU0HC4Hw8mqc60dzfEg4PYZVYMPiUan9DzA,47
itp_interface/tools/repl/test/file.lean,sha256=8z-cjiSdD0PTJm0tfJr_UDAxYmtWL7ii5HvVesxi5ns,70
itp_interface/tools/repl/test/have_by_sorry.expected.out,sha256=jRTHam3GRLSZj1F3Hnujy_D47Atj3PDmEfAs8RRY9zU,820
itp_interface/tools/repl/test/have_by_sorry.in,sha256=-HiIFL0u6XDrSyJJxEeGhUPNn6wjFtLzP5LHs26Uf1c,192
itp_interface/tools/repl/test/import_lean.expected.out,sha256=bZwUHIcXc9ENfG9oPBGKB_fDYtIfDi8jmd5durqJylo,12
itp_interface/tools/repl/test/import_lean.in,sha256=ZXglsGn75acpOMahmlp8vXDxpxE9NN2h48QDgWO4_E8,24
itp_interface/tools/repl/test/incomplete.expected.out,sha256=eBveOkX-BVEZwrP3bpdfFYcyTRSRnwwdMbmojZU1ZLE,548
itp_interface/tools/repl/test/incomplete.in,sha256=TtnbkU0mLJjGKR4rImSQ3O5UysYX5ZnpUL9iPNQmjYY,121
itp_interface/tools/repl/test/incomplete.lean,sha256=47DEQpj8HBSa-_TImW-5JCeuQeRkm5NMpJWZG3hSuFU,0
itp_interface/tools/repl/test/infotree.expected.out,sha256=xTrYwGklVo6_WOWbWZgZi_Bngu9F5vQyta_c9vQsWjI,591
itp_interface/tools/repl/test/infotree.in,sha256=Vq9yzvspj1BaaINvusb4253-cPuEuejJTvYj5xIHPyQ,79
itp_interface/tools/repl/test/invalid_tactic.expected.out,sha256=PiyRy2Iqz4nhoc1ZIDHZy6PwBb-G53jx4JLn6CuSjhU,556
itp_interface/tools/repl/test/invalid_tactic.in,sha256=SgRVAir5kn0PAA-w4g-BnwW4EZS0RvUaVFr_wpWWm8k,114
itp_interface/tools/repl/test/name_generator.expected.out,sha256=3IeQt2jByAkJskwrV-XIUlYYZ2a22_rPvrZmadm2QTo,1935
itp_interface/tools/repl/test/name_generator.in,sha256=YuUWWUP6SJwGFHSvNWjhfQbJYC5TbmRUx0Djn3f1kc0,578
itp_interface/tools/repl/test/no_goal_sorry.expected.out,sha256=3BfTJgvZVzGoQFx-vOvFShJtAHWJMM8oqbVvbC8Jftk,363
itp_interface/tools/repl/test/no_goal_sorry.in,sha256=5gYCNhM5TNv3WtZHEDOxa7VM77qvV83sP7_A4C82M2k,74
itp_interface/tools/repl/test/no_goal_sorry_2.expected.out,sha256=hC1mEHqu-g3iRu4axr81C0bTikzQUYo1pwGN_NoaYZA,294
itp_interface/tools/repl/test/no_goal_sorry_2.in,sha256=kNd6HfBzaND5A_t-t3PbP2OkrF99zFhZp-Meq-dte1I,51
itp_interface/tools/repl/test/options.expected.out,sha256=y0AmQf4fo8w43VZNm87Ru1cTohHmBu0Y-e3FLzCY7JI,447
itp_interface/tools/repl/test/options.in,sha256=TG933yqDYvWpVYsald0e3Gw3VSUxcD0dOaVw3IhXB0E,109
itp_interface/tools/repl/test/pickle_environment.expected.out,sha256=KIVudHv9tQZamopmL5nhGFH6h4FT0Q2FpZMDMLOcU3c,48
itp_interface/tools/repl/test/pickle_environment.in,sha256=zUeWr2B-oSBh_Zl6H5lWu4VM005DywgXBT8uIvcUrkg,149
itp_interface/tools/repl/test/pickle_environment_with_imports.expected.out,sha256=EBWr72rVwKogxQO27B-Nl8gTi2RztBDMnFdXKMMjKPs,60
itp_interface/tools/repl/test/pickle_environment_with_imports.in,sha256=2EN-dZV6PaezCXFmWcaomBHY-slQcCOp71KOJ0Lx1p4,183
itp_interface/tools/repl/test/pickle_open.expected.out,sha256=sJdocb6RIMh-hJUFYbkURcr_I-wVnOLpg9ppc3KagMg,48
itp_interface/tools/repl/test/pickle_open.in,sha256=PzwITCprt1c9jvLEpwNb4tvwZhrTUwnEvEsZkry788s,146
itp_interface/tools/repl/test/pickle_open_2.expected.out,sha256=WBzCu9vpOqnS7W5jF28xKjO9uqco3UDVVP2xwe7yR2I,24
itp_interface/tools/repl/test/pickle_open_2.in,sha256=62Lf_-xn1WExDvcp-7RrIzvhQob_XRZKU6OEg86H3Zo,82
itp_interface/tools/repl/test/pickle_open_scoped.expected.out,sha256=IbmOGA0dWiBABpWDuvu2OeNPmdhNnGBDwUHJJvFpNY4,337
itp_interface/tools/repl/test/pickle_open_scoped.in,sha256=OfgHwDAfTCyu9JhCNga-VaQd5ItuQTD7R_fA4TPZK2U,157
itp_interface/tools/repl/test/pickle_open_scoped_2.expected.out,sha256=N2VNAji2c8suABekaHdEkyEWceyWkpHWd_rmlNS0aRo,313
itp_interface/tools/repl/test/pickle_open_scoped_2.in,sha256=Ph-zGJuX32H5GtRkFjF3F6nZqs01mf_1mqeGYRd0yo8,88
itp_interface/tools/repl/test/pickle_proof_state_1.expected.out,sha256=Wx4bdp08DL-EvIm8Rbq46OV_AYEg-unVgxTkmb-IQL0,854
itp_interface/tools/repl/test/pickle_proof_state_1.in,sha256=01W4ymneqt_s5EZSllOgrLgIsR0Sk9k1QfYULl5dR08,344
itp_interface/tools/repl/test/pickle_proof_state_2.expected.out,sha256=uHoyDlF-h9xDGsM5FLWsKOWdKSCnmajGzcPJuMZR3QU,160
itp_interface/tools/repl/test/pickle_proof_state_2.in,sha256=v8CKqf83luvHG0wfB5IlUXpkbaRJnkdHv_XO_scuDgk,83
itp_interface/tools/repl/test/pickle_proof_state_env.expected.out,sha256=Wx4bdp08DL-EvIm8Rbq46OV_AYEg-unVgxTkmb-IQL0,854
itp_interface/tools/repl/test/pickle_proof_state_env.in,sha256=XdLjfFpAyLHTgF-tKQ92OF7nNnexxDao8vFZ77jdPUA,364
itp_interface/tools/repl/test/pickle_scoped_notation.in,sha256=zJJMgI3B20vvB31kj8h2YB3-KUqvHG-agAdm08-OMWU,310
itp_interface/tools/repl/test/pickle_scoped_notation_2.in,sha256=t8n30u5D2t_WS7dzUEGCuhVT5JSllBoP9E1TXIiS7_U,84
itp_interface/tools/repl/test/proof_branching.expected.out,sha256=pihdRRKQHrbUh1mhdPN74LvTkyoMUxxkBwdsJwRRQfE,901
itp_interface/tools/repl/test/proof_branching.in,sha256=JB2wrXqrc7ZWtDzPNLDbhzzVVZGc3s-k_FRt9Zy_Buc,281
itp_interface/tools/repl/test/proof_branching2.expected.out,sha256=eQls6Czdce44mzGWnvkiaqI8VzznYibdWmWUG7PFMxY,1120
itp_interface/tools/repl/test/proof_branching2.in,sha256=-ExLEKdFxXOUhV3aSzrcKva7qsL-I13xFTA-Dvi548A,346
itp_interface/tools/repl/test/proof_step.expected.out,sha256=VYmOsddqgygPMSAPz9rA_Bzd9pAh8mM29jrWwqEjKY0,551
itp_interface/tools/repl/test/proof_step.in,sha256=M3zfMaxksPqriZ0eIwH7He7jd--4o5kDgutocrIA6vo,176
itp_interface/tools/repl/test/proof_transitivity.expected.out,sha256=lkG8vRKfbFeNmAXD23_MCcwpBzThoTBbbrExDL8Mfe0,802
itp_interface/tools/repl/test/proof_transitivity.in,sha256=GZHfnJtiJu4JqyfD2pWISnmTHMSaprtcYCXbnId6UXY,268
itp_interface/tools/repl/test/readme.expected.out,sha256=X-Gd7gEJfR-iyWIu4pwA5KKAdT9e3GRL0SuAk4Wjk7U,471
itp_interface/tools/repl/test/readme.in,sha256=X7ZeO2dgJYzVWI3pUQZ9BHq1nOr8SEjcbhfNX2PEBSY,138
itp_interface/tools/repl/test/root_goals.expected.out,sha256=6-6bcDXIGmbQ5AyMMOoWUCsfVAHVXNvTwSJSzASxGMI,540
itp_interface/tools/repl/test/root_goals.in,sha256=_aoIEKZg0x5gkzAyvMb6dyn9lL-0h7QXdJZuhFfOj-8,181
itp_interface/tools/repl/test/self_proof_apply_check.expected.out,sha256=9te2x7NmFn6EGAwWElJRjkWXF1CDdw8oXA2z8uXZZ6o,810
itp_interface/tools/repl/test/self_proof_apply_check.in,sha256=5xUj8IIt2U1shl1og0BynQkDSBuZ7FgKOK8QdDxv290,126
itp_interface/tools/repl/test/self_proof_check.expected.out,sha256=tWAU0zGMNwClmxHnC0qLZN8M0n5TE1WGmJCfQ3v9qxs,2340
itp_interface/tools/repl/test/self_proof_check.in,sha256=iP8ybxz7fyHd3XRmY_TeR6tulsWZemoSdNC0501dlYA,408
itp_interface/tools/repl/test/self_proof_exact_check.expected.out,sha256=9te2x7NmFn6EGAwWElJRjkWXF1CDdw8oXA2z8uXZZ6o,810
itp_interface/tools/repl/test/self_proof_exact_check.in,sha256=nvyaqQVBZC86hDVqL6HlAko7BZ8e1BJ0LAhXJRiK5kI,126
itp_interface/tools/repl/test/self_proof_rw.expected.out,sha256=up6wuUZOdrzw7iFtlgVEO_GhLXKuW_PQzBJC9H4XxCY,838
itp_interface/tools/repl/test/self_proof_rw.in,sha256=9e8gHsUxq6QHw33aNPnNudZzHJ8VXQL3Obre_dbHzFY,183
itp_interface/tools/repl/test/sorry_hypotheses.expected.out,sha256=1Z_Z0EIruATPi9i04Kj_xd0WZQ7I65fqLafvnPHprWE,488
itp_interface/tools/repl/test/sorry_hypotheses.in,sha256=hPXGN4jyrYkQdS597uF-fQVzjla_pOjOA9FQf5D72FQ,111
itp_interface/tools/repl/test/synthesize_placeholder.expected.out,sha256=lEGc5EfvyPV6gWoaT2Rrt7MFYqf6o3EYL4iLdQplvXs,202
itp_interface/tools/repl/test/synthesize_placeholder.in,sha256=qapdR7L57dVDK5xGF9p4nOo4N6MY2s6Qc7LWh2wySdk,28
itp_interface/tools/repl/test/tactic_mode_sorry.expected.out,sha256=FVjRDiyKs0FqKi1nlF_j0PnNLZ4e8pqorr_NjfzIyKc,431
itp_interface/tools/repl/test/tactic_mode_sorry.in,sha256=OnbTqShdFsb3J7bKHoQwCMBeV3-Cv99YXy8wSL3AWcA,73
itp_interface/tools/repl/test/tactic_sorry.expected.out,sha256=wExThghHHP1cCMEr4F-zEdMkb5hMc4qsUTD7g6m6mqw,300
itp_interface/tools/repl/test/tactic_sorry.in,sha256=aaqWiqqumms7UaTtTjwSeLt0RCRIfI4i7ANtK-8CZ9U,35
itp_interface/tools/repl/test/term_sorry.expected.out,sha256=JD2Rd9UFO6zf9_KNUf_Csl0pyoPFwYGPxtrH6JyPXNo,300
itp_interface/tools/repl/test/term_sorry.in,sha256=eEiaAWb96dPeGEFRm0xKsKLeQWT0Spr3jiLWkxjjJVg,32
itp_interface/tools/repl/test/trace_simp.expected.out,sha256=wGdIewLfeiKYHiAB4lrLwvjYo_OEnMc8bBnSDgFXYsI,1110
itp_interface/tools/repl/test/trace_simp.in,sha256=S9zg4CV90HBWaGMxehSndDdIT7wANYfSxFrkVCfyhWQ,389
itp_interface/tools/repl/test/unfinished_tactic_block.expected.out,sha256=04F4tAw7KyUgjcD40GJZUKttiMJkfncAIX9fMbk-NJE,299
itp_interface/tools/repl/test/unfinished_tactic_block.in,sha256=Z-lSdemNLocjNk5Zsbx7bo-tOtVMENpCnerwhGfH3sI,29
itp_interface/tools/repl/test/unknown_environment.expected.out,sha256=ruH7s89H_HUXtOr0g6uJw_xIof2Ll5RDakXAPWfaPoE,37
itp_interface/tools/repl/test/unknown_environment.in,sha256=XX8PjA9vdd27DXYnMYYXeYJBx_Gc05qTL1l7MlXZjQA,45
itp_interface/tools/repl/test/unknown_proof_state.expected.out,sha256=jk7-V4PE2mkTlrxx9Qo45zJQ4alHy6voYfP4kDrBmL4,337
itp_interface/tools/repl/test/unknown_proof_state.in,sha256=SPwS6pWa_t5yPM1195zaExPwDaGkwj4CyHc490hQBWs,77
itp_interface/tools/repl/test/unknown_tactic.expected.out,sha256=xFE3uJ6oSOZg4ifSOiHJIwfhym7swNMonLpVVKFrqFQ,357
itp_interface/tools/repl/test/unknown_tactic.in,sha256=HY1oE_7an4Xey8Bym2gB8lfdcnCw2j-hKpdHQxQ7tqU,76
itp_interface/tools/repl/test/variables.expected.out,sha256=zmB9YOCtKCOD3jennIQtEF9_kDdyZvElANi8vLVZFtY,673
itp_interface/tools/repl/test/variables.in,sha256=2Mp3QDtTvUppQVUxZz3tnUKnVf5YK-XgL5fnhl9EZqA,237
itp_interface/tools/repl/test/Mathlib/.gitignore,sha256=4zIzbyKXApFqgDE8l3uo9OGKfRvuYvP2AN3HXjiH0Y0,72
itp_interface/tools/repl/test/Mathlib/H20231110.sh,sha256=fh1WzHusunE0Hyz8jSjDZiVe2rniYx9sH79tXETu5NA,120
itp_interface/tools/repl/test/Mathlib/ReplMathlibTests.lean,sha256=EBX49GdqJ-pjeAswzJFnEiMoVwl7K99jXcYcuUnBB_s,15
itp_interface/tools/repl/test/Mathlib/lake-manifest.json,sha256=FpcvDiNvuhX3dc41qvTq7GKdjEzfzY_6Mxmucx4JxA8,3110
itp_interface/tools/repl/test/Mathlib/lakefile.toml,sha256=Zd6am8OrE4scLr5MSYZIdFN98A6LQP3PM9o6a-os_xA,232
itp_interface/tools/repl/test/Mathlib/lean-toolchain,sha256=0k_tQ007E636q1dySgp_Jw6ovxyBi1rlzyXLziTdaFw,25
itp_interface/tools/repl/test/Mathlib/test.sh,sha256=wR6a80sX2wBESnSGpg97djXHprWaX_udRdw8dRshWcU,1120
itp_interface/tools/repl/test/Mathlib/test/20240209.expected.out,sha256=OL0cBxPASvkY9kJVf3QKpC1MjHFakX4RM0-XlRzZXrs,535
itp_interface/tools/repl/test/Mathlib/test/20240209.in,sha256=yt76LmeaXAXIrg7X-6DcO1fqWavnp7X8ZmG4kHTk79U,102
itp_interface/tools/repl/test/Mathlib/test/20240209.lean,sha256=z6BqnOJfmkKbTBYbd_f9Z_pTDu6dWH-ixKuPe1GAU_4,55
itp_interface/tools/repl/test/Mathlib/test/H20231020.expected.out,sha256=JIj77iGXLnP5vlSmtO6tYkCkXxWzK6T7lU5EUTJiMfg,48
itp_interface/tools/repl/test/Mathlib/test/H20231020.in,sha256=ltnsNyxkyXVHqIGKg_opdr34VbnJidSDtgiWLSyfHXg,892
itp_interface/tools/repl/test/Mathlib/test/H20231020.lean,sha256=YQXP4W8t-1Qi2PgIMPstHINogdA8mQQpw3fOlYY15jc,797
itp_interface/tools/repl/test/Mathlib/test/H20231110.expected.out,sha256=WBzCu9vpOqnS7W5jF28xKjO9uqco3UDVVP2xwe7yR2I,24
itp_interface/tools/repl/test/Mathlib/test/H20231110.in,sha256=kX42DYKDWmNqyqOrEY2TmTH_2yL6nwo8q_f3mUPFzHc,368
itp_interface/tools/repl/test/Mathlib/test/H20231115.expected.out,sha256=fy4yMUn4puAyTw1Ba9MYnGZt_R7IkuapwkZUQ4oHMdM,499
itp_interface/tools/repl/test/Mathlib/test/H20231115.in,sha256=WaZP0FoHV_nzJxZg1xbMs0dKkzFewsnF5DORiauPLWs,158
itp_interface/tools/repl/test/Mathlib/test/H20231115_2.expected.out,sha256=CrzV7eoObxiUxGvv5WM-QDICbIj8mcWB8PLOquDBlYQ,499
itp_interface/tools/repl/test/Mathlib/test/H20231115_2.in,sha256=blx8N5WjBV7MyqMWfcSXBg8ZQSNyK7cP7pU0KSpv9Sk,143
itp_interface/tools/repl/test/Mathlib/test/H20231115_3.expected.out,sha256=-qSw4lXZjWekf-c4AKItYU2BS_axFKAgJTpLxKA7fLc,259
itp_interface/tools/repl/test/Mathlib/test/H20231115_3.in,sha256=yU-v5Yu98IpdUHM0l4_ajFLeRgUgZWT8xzSSqsO3y48,124
itp_interface/tools/repl/test/Mathlib/test/H20231214.in,sha256=_Z7sLyE0LUQeik5rfAedOh10nu7Ix4OWB-rA3ueWKYU,481
itp_interface/tools/repl/test/Mathlib/test/H20231214.lean,sha256=VuUOy1Y1ur4wUTZETpxHvhbNg7Ao6XqPupSwiczKMFM,826
itp_interface/tools/repl/test/Mathlib/test/H20231215.expected.out,sha256=XHGkNeBBF2tUJw0NjzSpPttSF5vUbV9qaiSkXZbQbMg,24
itp_interface/tools/repl/test/Mathlib/test/H20231215.in,sha256=DYRxEbbUoaOO3db_ww4nbVPOGZnxVPL46C1WHliJuAc,115
itp_interface/tools/repl/test/Mathlib/test/H20231215_2.expected.out,sha256=n3oL4RcF2VVUdQkE3W_lKJgBvQ18xxE3Ii-h4zfEaL4,321
itp_interface/tools/repl/test/Mathlib/test/H20231215_2.in,sha256=RwOEhr1JU5dRxrp-rpLj3myUIfl9325cJkJ0sgfNqEQ,126
itp_interface/tools/repl/test/Mathlib/test/exact.expected.out,sha256=c1_UNn_uaUWEuSytIhXPetPoF8OvjoKEn-bhqGToaVQ,941
itp_interface/tools/repl/test/Mathlib/test/exact.in,sha256=zHiyj00tsIuwMmQRfew1Uu3Cr5cR80eue_QMsD_eZgY,215
itp_interface/tools/repl/test/Mathlib/test/import_Mathlib.lean,sha256=EBX49GdqJ-pjeAswzJFnEiMoVwl7K99jXcYcuUnBB_s,15
itp_interface/tools/repl/test/Mathlib/test/induction.expected.out,sha256=UOwEfSNO_GX9XAoD9ije392kivnMDS1FX7zO94wGxgg,878
itp_interface/tools/repl/test/Mathlib/test/induction.in,sha256=essP7h1h-eVmRYCwDf4tX2PteQwTpJx6BvtAwGRc6ko,268
itp_interface/tools/repl/test/Mathlib/test/induction.lean,sha256=J-_5QnoGVoWvGk_MZsQiQqiqIUPMWI1LOaXk5jiD1zw,112
itp_interface/tools/repl/test/Mathlib/test/on_goal.expected.out,sha256=ND_fbspbSldHsFZcPWvDz2FMLr0wshnvWrBN9ft3Qoc,765
itp_interface/tools/repl/test/Mathlib/test/on_goal.in,sha256=aeYwHa_1bhrElSMkS0P8EV9kU2tc_I-g14O2mc0wj2Y,259
itp_interface/tools/repl/test/Mathlib/test/pickle.expected.out,sha256=y83wg52vjE3jYFJt3DtjBZKGETBHbswgjhmSPKCW7kQ,494
itp_interface/tools/repl/test/Mathlib/test/pickle.in,sha256=sNiZED6ATOmn0p8VZq6pO1czKV1OcigCsR9pmj2fldU,241
itp_interface/tools/repl/test/Mathlib/test/pickle_2.expected.out,sha256=pEXa5E4sqJXjUqj73p2X2FLmYNDGreeVEl2jtfQh2E8,272
itp_interface/tools/repl/test/Mathlib/test/pickle_2.in,sha256=I67KImQsl4UskMK3vU7Tl_5BL8jVIHtoqW9Zl0gjVkg,95
itp_interface/tools/repl/test/Mathlib/test/placeholder_synthesis.expected.out,sha256=k0y2D2tiCP8ggOsRlpvMeN0-QgMNhDdYvfc5D41Xu0U,759
itp_interface/tools/repl/test/Mathlib/test/placeholder_synthesis.in,sha256=cTsCB_MDByAhbL5mrJR0TmucnQEFeJPNAyuxAz2zrbs,281
itp_interface-1.5.0.dist-info/METADATA,sha256=X3dtucSRztI78bSdRPaq-4O94eeHosqGynAOfIUd21Y,13469
itp_interface-1.5.0.dist-info/WHEEL,sha256=WLgqFyCfm_KASv4WHyYy0P3pM_m7J5L9k2skdKLirC8,87
itp_interface-1.5.0.dist-info/entry_points.txt,sha256=Lkhj6Yrocknc8LsSbf2KV-dBP7KQWWYyqjnbS10dLjI,217
itp_interface-1.5.0.dist-info/licenses/LICENSE,sha256=Ja0zK0mghvyO3342OSoi9LPoKvj92RqN17fXcYOcMME,1066
itp_interface-1.5.0.dist-info/RECORD,,
