Created
September 25, 2018 04:02
-
-
Save kckennylau/6d1e02b8289f24be38416642b5d91142 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ /c/lean/bin/lean --profile algebra/big_operators.lean | |
| parsing took 1.14ms | |
| type checking of directed.finset_le took 0.239ms | |
| compilation of directed.finset_le took 0.00302ms | |
| decl post-processing of directed.finset_le took 0.0143ms | |
| parsing took 0.16ms | |
| elaboration of prod took 0.553ms | |
| type checking of prod took 0.111ms | |
| compilation of finset.prod took 1.5ms | |
| elaboration of directed.finset_le took 12.3ms | |
| decl post-processing of prod took 152ms | |
| parsing took 0.241ms | |
| type checking of prod_eq_fold took 0.607ms | |
| compilation of finset.prod_eq_fold took 0.00151ms | |
| elaboration of prod_eq_fold took 0.769ms | |
| decl post-processing of prod_eq_fold took 148ms | |
| parsing took 0.0955ms | |
| type checking of prod_empty took 0.107ms | |
| compilation of finset.prod_empty took 0.00151ms | |
| elaboration of prod_empty took 0.933ms | |
| decl post-processing of prod_empty took 127ms | |
| parsing took 0.172ms | |
| type checking of prod_insert took 0.202ms | |
| compilation of finset.prod_insert took 0.0143ms | |
| elaboration of prod_insert took 81.9ms | |
| decl post-processing of prod_insert took 140ms | |
| parsing took 0.088ms | |
| type checking of prod_singleton took 0.0544ms | |
| compilation of finset.prod_singleton took 0.00113ms | |
| elaboration of prod_singleton took 93.3ms | |
| decl post-processing of prod_singleton took 142ms | |
| parsing took 5.05ms | |
| type checking of prod_const_one took 0.0914ms | |
| compilation of finset.prod_const_one took 0.00151ms | |
| decl post-processing of prod_const_one took 0.197ms | |
| parsing took 0.139ms | |
| elaboration: tactic compilation took 4.62ms | |
| elaboration: tactic execution took 15ms | |
| num. allocated objects: 173 | |
| num. allocated closures: 172 | |
| 15ms 100.0% tactic.interactive.simp_core | |
| 15ms 100.0% tactic.step | |
| 15ms 100.0% tactic.interactive.propagate_tags | |
| 15ms 100.0% _interaction._lambda_2 | |
| 15ms 100.0% tactic.istep | |
| 15ms 100.0% tactic.istep._lambda_1 | |
| 15ms 100.0% scope_trace | |
| 15ms 100.0% interaction_monad_orelse | |
| 14ms 93.3% tactic.interactive.simp_core_aux | |
| 14ms 93.3% tactic.simp_target | |
| 14ms 93.3% tactic.interactive.simp_core_aux._lambda_5 | |
| 14ms 93.3% tactic.simplify | |
| 1ms 6.7% simp_lemmas.add_pexpr | |
| 1ms 6.7% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 1ms 6.7% tactic.try | |
| 1ms 6.7% tactic.try_core | |
| 1ms 6.7% simp_lemmas.resolve_and_add | |
| 1ms 6.7% tactic.save_const_type_info._lambda_1 | |
| 1ms 6.7% simp_lemmas.append_pexprs | |
| 1ms 6.7% tactic.save_type_info | |
| 1ms 6.7% tactic.mk_simp_set | |
| 1ms 6.7% tactic.mk_simp_set_core | |
| elaboration of prod_const_one took 32.7ms | |
| type checking of sum_const_zero took 0.0899ms | |
| compilation of finset.sum_const_zero took 0.00151ms | |
| decl post-processing of sum_const_zero took 0.245ms | |
| elaboration of sum_const_zero took 3.12ms | |
| parsing took 0.493ms | |
| type checking of prod_image took 0.537ms | |
| compilation of finset.prod_image took 0.00378ms | |
| elaboration of prod_image took 132ms | |
| decl post-processing of prod_image took 219ms | |
| parsing took 2.08ms | |
| type checking of prod_congr took 0.106ms | |
| compilation of finset.prod_congr took 0.00151ms | |
| elaboration: tactic compilation took 4.59ms | |
| elaboration: tactic execution took 65ms | |
| num. allocated objects: 107 | |
| num. allocated closures: 125 | |
| 65ms 100.0% tactic.step | |
| 65ms 100.0% scope_trace | |
| 65ms 100.0% tactic.istep._lambda_1 | |
| 65ms 100.0% all_goals_core | |
| 65ms 100.0% tactic.istep | |
| 65ms 100.0% tactic.seq | |
| 65ms 100.0% tactic.all_goals | |
| 65ms 100.0% interaction_monad.monad._lambda_9 | |
| 65ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 65ms 100.0% tactic.interactive.exact | |
| 60ms 92.3% tactic.to_expr | |
| 5ms 7.7% tactic.exact | |
| elaboration of prod_congr took 111ms | |
| decl post-processing of prod_congr took 157ms | |
| parsing took 0.197ms | |
| type checking of prod_union_inter took 0.451ms | |
| compilation of finset.prod_union_inter took 0.00227ms | |
| elaboration of prod_union_inter took 118ms | |
| decl post-processing of prod_union_inter took 199ms | |
| parsing took 3.11ms | |
| type checking of prod_union took 0.247ms | |
| compilation of finset.prod_union took 0.00189ms | |
| elaboration: tactic compilation took 5.18ms | |
| elaboration: tactic execution took 10ms | |
| num. allocated objects: 195 | |
| num. allocated closures: 182 | |
| 10ms 100.0% interaction_monad.monad._lambda_9 | |
| 10ms 100.0% tactic.seq | |
| 10ms 100.0% tactic.istep | |
| 10ms 100.0% tactic.step | |
| 10ms 100.0% tactic.istep._lambda_1 | |
| 10ms 100.0% scope_trace | |
| 9ms 90.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 9ms 90.0% all_goals_core | |
| 9ms 90.0% tactic.interactive.exact | |
| 9ms 90.0% tactic.all_goals | |
| 9ms 90.0% tactic.to_expr | |
| 1ms 10.0% _private.3132620493.rw_goal._lambda_4 | |
| 1ms 10.0% rw_core | |
| 1ms 10.0% tactic.rewrite | |
| 1ms 10.0% interaction_monad.orelse' | |
| 1ms 10.0% tactic.interactive.propagate_tags | |
| 1ms 10.0% _private.3132620493.rw_goal._lambda_2 | |
| 1ms 10.0% tactic.rewrite_target | |
| 1ms 10.0% tactic.rewrite_core | |
| 1ms 10.0% _interaction._lambda_2 | |
| 1ms 10.0% interactive.loc.apply | |
| elaboration of prod_union took 27.2ms | |
| decl post-processing of prod_union took 137ms | |
| parsing took 3.13ms | |
| type checking of prod_sdiff took 0.221ms | |
| compilation of finset.prod_sdiff took 0.00227ms | |
| elaboration: tactic compilation took 4.43ms | |
| elaboration: tactic execution took 4ms | |
| num. allocated objects: 121 | |
| num. allocated closures: 124 | |
| 4ms 100.0% rw_core | |
| 4ms 100.0% interaction_monad.monad._lambda_9 | |
| 4ms 100.0% interactive.loc.apply | |
| 4ms 100.0% tactic.step | |
| 4ms 100.0% tactic.interactive.propagate_tags | |
| 4ms 100.0% _interaction._lambda_2 | |
| 4ms 100.0% _private.3132620493.rw_goal._lambda_4 | |
| 4ms 100.0% tactic.istep | |
| 4ms 100.0% tactic.istep._lambda_1 | |
| 4ms 100.0% scope_trace | |
| 4ms 100.0% interaction_monad.orelse' | |
| 4ms 100.0% _private.3132620493.rw_goal._lambda_2 | |
| 2ms 50.0% tactic.interactive.to_expr' | |
| 2ms 50.0% tactic.to_expr | |
| 2ms 50.0% tactic.rewrite_target | |
| 1ms 25.0% tactic.mk_eq_mpr | |
| 1ms 25.0% tactic.rewrite | |
| 1ms 25.0% tactic.rewrite_core | |
| 1ms 25.0% tactic.replace_target | |
| elaboration of prod_sdiff took 16.4ms | |
| decl post-processing of prod_sdiff took 218ms | |
| eq_empty_of_forall_not_mem : (∀ (x : ?M_1), x ∉ ?M_2) → ?M_2 = ∅ | |
| parsing took 27.3ms | |
| type checking of prod_bind took 0.643ms | |
| compilation of finset.prod_bind took 0.0034ms | |
| elaboration: tactic compilation took 8.15ms | |
| elaboration: tactic compilation took 4.21ms | |
| elaboration: tactic execution took 17ms | |
| num. allocated objects: 133 | |
| num. allocated closures: 119 | |
| 17ms 100.0% _interaction._lambda_2 | |
| 17ms 100.0% tactic.step | |
| 17ms 100.0% tactic.istep._lambda_1 | |
| 17ms 100.0% scope_trace | |
| 17ms 100.0% tactic.interactive.propagate_tags | |
| 17ms 100.0% tactic.interactive.simp_core | |
| 17ms 100.0% tactic.istep | |
| 16ms 94.1% tactic.interactive.simp_core_aux._lambda_5 | |
| 16ms 94.1% tactic.interactive.simp_core_aux | |
| 16ms 94.1% tactic.simp_target | |
| 16ms 94.1% interaction_monad_orelse | |
| 14ms 82.4% tactic.simplify | |
| 2ms 11.8% tactic.replace_target | |
| 2ms 11.8% tactic.mk_eq_mpr | |
| 1ms 5.9% simp_lemmas.add_pexpr | |
| 1ms 5.9% report_invalid_simp_lemma | |
| 1ms 5.9% to_fmt | |
| 1ms 5.9% simp_lemmas.append_pexprs | |
| 1ms 5.9% name.has_to_format | |
| 1ms 5.9% name.to_string_with_sep | |
| 1ms 5.9% simp_lemmas.resolve_and_add | |
| 1ms 5.9% tactic.mk_simp_set | |
| 1ms 5.9% tactic.mk_simp_set_core | |
| elaboration: tactic compilation took 9.68ms | |
| elaboration: tactic execution took 10ms | |
| num. allocated objects: 509 | |
| num. allocated closures: 439 | |
| 10ms 100.0% scope_trace | |
| 10ms 100.0% interaction_monad.monad._lambda_9 | |
| 10ms 100.0% tactic.istep | |
| 10ms 100.0% tactic.step | |
| 10ms 100.0% tactic.istep._lambda_1 | |
| 10ms 100.0% tactic.seq | |
| 8ms 80.0% tactic.all_goals | |
| 8ms 80.0% all_goals_core | |
| 8ms 80.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 4ms 40.0% tactic.rcases_core | |
| 4ms 40.0% tactic.to_expr | |
| 4ms 40.0% tactic.focus1 | |
| 4ms 40.0% tactic.rcases_core._main._lambda_5 | |
| 4ms 40.0% tactic.interactive.rintro | |
| 4ms 40.0% tactic.rintro | |
| 4ms 40.0% tactic.rintro._lambda_3 | |
| 4ms 40.0% tactic.rcases.continue | |
| 4ms 40.0% tactic.interactive.exact | |
| 3ms 30.0% tactic.rcases_core._main._lambda_2 | |
| 3ms 30.0% tactic.rcases_core._main._lambda_3 | |
| 3ms 30.0% tactic.cases_core | |
| 2ms 20.0% interaction_monad.orelse' | |
| 2ms 20.0% _private.3132620493.rw_goal._lambda_4 | |
| 2ms 20.0% _private.3132620493.rw_goal._lambda_2 | |
| 2ms 20.0% tactic.rewrite_target | |
| 2ms 20.0% interactive.loc.apply | |
| 2ms 20.0% rw_core | |
| 2ms 20.0% tactic.interactive.propagate_tags | |
| 2ms 20.0% _interaction._lambda_2 | |
| 1ms 10.0% tactic.replace_target | |
| 1ms 10.0% tactic.has_opt_auto_param._lambda_2 | |
| 1ms 10.0% tactic.infer_type | |
| 1ms 10.0% tactic.rewrite | |
| 1ms 10.0% tactic.assert_core | |
| 1ms 10.0% tactic.assert | |
| 1ms 10.0% to_fmt | |
| 1ms 10.0% expr.has_to_format | |
| 1ms 10.0% expr.to_string | |
| elaboration: tactic compilation took 5.44ms | |
| elaboration: tactic execution took 28ms | |
| num. allocated objects: 129 | |
| num. allocated closures: 97 | |
| 28ms 100.0% tactic.interactive.simp_core | |
| 28ms 100.0% tactic.step | |
| 28ms 100.0% _interaction._lambda_2 | |
| 28ms 100.0% tactic.istep._lambda_1 | |
| 28ms 100.0% tactic.interactive.propagate_tags | |
| 28ms 100.0% scope_trace | |
| 28ms 100.0% tactic.istep | |
| 26ms 92.9% interaction_monad_orelse | |
| 25ms 89.3% tactic.interactive.simp_core_aux._lambda_5 | |
| 25ms 89.3% tactic.interactive.simp_core_aux | |
| 25ms 89.3% tactic.simp_target | |
| 23ms 82.1% tactic.simplify | |
| 3ms 10.7% tactic.mk_simp_set_core | |
| 3ms 10.7% simp_lemmas.add_pexpr | |
| 3ms 10.7% simp_lemmas.append_pexprs | |
| 3ms 10.7% tactic.mk_simp_set | |
| 2ms 7.1% tactic.to_expr | |
| 2ms 7.1% tactic.replace_target | |
| 2ms 7.1% tactic.mk_app | |
| 2ms 7.1% tactic.mk_id_eq | |
| 1ms 3.6% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 1ms 3.6% simp_lemmas.resolve_and_add | |
| 1ms 3.6% simp_lemmas.add_simp | |
| decl post-processing of prod_bind took 166ms | |
| elaboration: tactic execution took 100ms | |
| num. allocated objects: 31 | |
| num. allocated closures: 39 | |
| 100ms 100.0% tactic.step | |
| 100ms 100.0% scope_trace | |
| 100ms 100.0% tactic.istep._lambda_1 | |
| 100ms 100.0% all_goals_core | |
| 100ms 100.0% tactic.istep | |
| 100ms 100.0% tactic.seq | |
| 100ms 100.0% tactic.all_goals | |
| 100ms 100.0% interaction_monad.monad._lambda_9 | |
| 100ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 100ms 100.0% tactic.interactive.exact | |
| 99ms 99.0% tactic.to_expr | |
| 1ms 1.0% tactic.exact | |
| elaboration of prod_bind took 169ms | |
| parsing took 42.4ms | |
| type checking of prod_product took 0.163ms | |
| compilation of finset.prod_product took 0.00113ms | |
| elaboration: tactic compilation took 10.8ms | |
| decl post-processing of prod_product took 164ms | |
| elaboration: tactic execution took 98ms | |
| num. allocated objects: 1488 | |
| num. allocated closures: 1274 | |
| 98ms 100.0% tactic.istep | |
| 98ms 100.0% _interaction._lambda_2 | |
| 98ms 100.0% scope_trace | |
| 98ms 100.0% tactic.istep._lambda_1 | |
| 98ms 100.0% tactic.step | |
| 33ms 33.7% interaction_monad_orelse | |
| 33ms 33.7% tactic.cc_core | |
| 32ms 32.7% cc_state.mk_using_hs_core | |
| 32ms 32.7% tactic.solve1 | |
| 27ms 27.6% tactic.interactive.propagate_tags | |
| 22ms 22.4% tactic.interactive.simp_core | |
| 21ms 21.4% tactic.simp_target | |
| 21ms 21.4% tactic.interactive.simp_core_aux | |
| 21ms 21.4% tactic.interactive.simp_core_aux._lambda_5 | |
| 20ms 20.4% tactic.focus1 | |
| 19ms 19.4% tactic.simplify | |
| 16ms 16.3% tactic.to_expr | |
| 15ms 15.3% tactic.interactive.exact | |
| 14ms 14.3% interaction_monad.monad._lambda_9 | |
| 14ms 14.3% tactic.congr._main._lambda_2 | |
| 9ms 9.2% tactic.congr_core | |
| 9ms 9.2% tactic.apply_eq_congr_core | |
| 7ms 7.1% tactic.try_core | |
| 7ms 7.1% tactic.try | |
| 7ms 7.1% tactic.mk_specialized_congr_lemma | |
| 6ms 6.1% tactic.rcases_core._main._lambda_5 | |
| 6ms 6.1% tactic.rintro | |
| 6ms 6.1% tactic.rcases_core | |
| 6ms 6.1% tactic.interactive.rintro | |
| 6ms 6.1% tactic.rintro._lambda_3 | |
| 6ms 6.1% tactic.rcases.continue | |
| 5ms 5.1% interactive.loc.apply | |
| 5ms 5.1% interaction_monad.orelse' | |
| 5ms 5.1% _private.3132620493.rw_goal._lambda_4 | |
| 5ms 5.1% tactic.cases_core | |
| 5ms 5.1% rw_core | |
| 5ms 5.1% _private.3132620493.rw_goal._lambda_2 | |
| 5ms 5.1% tactic.apply_core | |
| 5ms 5.1% tactic.rcases_core._main._lambda_2 | |
| 5ms 5.1% tactic.rcases.continue._main._lambda_2 | |
| 5ms 5.1% tactic.replace_target | |
| 4ms 4.1% tactic.rewrite_target | |
| 4ms 4.1% tactic.rcases_core._main._lambda_3 | |
| 4ms 4.1% all_goals_core | |
| 4ms 4.1% tactic.apply | |
| 4ms 4.1% tactic.congr._main._lambda_1 | |
| 4ms 4.1% _private.3864167971.all_goals_core._main._lambda_2 | |
| 4ms 4.1% tactic.all_goals | |
| 3ms 3.1% tactic.assumption._lambda_1 | |
| 3ms 3.1% tactic.infer_type | |
| 3ms 3.1% tactic.find_same_type | |
| 3ms 3.1% tactic.exact | |
| 2ms 2.0% tactic.mk_eq_mpr | |
| 2ms 2.0% tactic.interactive.funext | |
| 2ms 2.0% relation_tactic | |
| 2ms 2.0% tactic.funext_core | |
| 2ms 2.0% tactic.funext_core._main._lambda_2 | |
| 2ms 2.0% tactic.applyc | |
| 2ms 2.0% _private.878893113.relation_tactic._lambda_1 | |
| 2ms 2.0% tactic.apply_congr_core | |
| 1ms 1.0% simp_lemmas.append_pexprs | |
| 1ms 1.0% tactic.cleanup | |
| 1ms 1.0% string.has_to_format | |
| 1ms 1.0% simp_lemmas.resolve_and_add | |
| 1ms 1.0% format.of_string | |
| 1ms 1.0% environment.get | |
| 1ms 1.0% report_invalid_simp_lemma | |
| 1ms 1.0% simp_lemmas.add_pexpr | |
| 1ms 1.0% tactic.mk_simp_set_core | |
| 1ms 1.0% tactic.set_goals | |
| 1ms 1.0% to_fmt | |
| 1ms 1.0% tactic.intro_core | |
| 1ms 1.0% tactic.assert | |
| 1ms 1.0% tactic.rewrite | |
| 1ms 1.0% tactic.mk_const | |
| 1ms 1.0% tactic.mk_simp_set | |
| 1ms 1.0% tactic.rewrite_core | |
| 1ms 1.0% tactic.intro | |
| 1ms 1.0% tactic.interactive.to_expr' | |
| elaboration of prod_product took 176ms | |
| parsing took 45.8ms | |
| type checking of prod_sigma took 0.235ms | |
| compilation of finset.prod_sigma took 0.00151ms | |
| elaboration: tactic compilation took 3.93ms | |
| elaboration: tactic compilation took 4.8ms | |
| elaboration: tactic execution took 2ms | |
| num. allocated objects: 62 | |
| num. allocated closures: 101 | |
| 2ms 100.0% tactic.rewrite | |
| 2ms 100.0% interaction_monad.monad._lambda_9 | |
| 2ms 100.0% interactive.loc.apply | |
| 2ms 100.0% tactic.step | |
| 2ms 100.0% tactic.interactive.propagate_tags | |
| 2ms 100.0% _interaction._lambda_2 | |
| 2ms 100.0% _private.3132620493.rw_goal._lambda_4 | |
| 2ms 100.0% tactic.istep | |
| 2ms 100.0% tactic.istep._lambda_1 | |
| 2ms 100.0% rw_core | |
| 2ms 100.0% scope_trace | |
| 2ms 100.0% interaction_monad.orelse' | |
| 2ms 100.0% _private.3132620493.rw_goal._lambda_2 | |
| 2ms 100.0% tactic.rewrite_target | |
| 1ms 50.0% tactic.infer_type | |
| 1ms 50.0% tactic.rewrite_core | |
| 1ms 50.0% tactic.has_opt_auto_param._lambda_2 | |
| elaboration: tactic compilation took 8.48ms | |
| decl post-processing of prod_sigma took 164ms | |
| parsing took 1.78ms | |
| type checking of prod_mul_distrib took 0.219ms | |
| compilation of finset.prod_mul_distrib took 0.00227ms | |
| elaboration: tactic execution took 104ms | |
| num. allocated objects: 816 | |
| num. allocated closures: 677 | |
| 104ms 100.0% scope_trace | |
| 104ms 100.0% tactic.step | |
| 104ms 100.0% tactic.istep._lambda_1 | |
| 104ms 100.0% tactic.seq | |
| 104ms 100.0% tactic.istep | |
| 76ms 73.1% interaction_monad.monad._lambda_9 | |
| 76ms 73.1% _private.3864167971.all_goals_core._main._lambda_2 | |
| 76ms 73.1% tactic.all_goals | |
| 76ms 73.1% all_goals_core | |
| 65ms 62.5% tactic.cc_core | |
| 64ms 61.5% cc_state.mk_using_hs_core | |
| 28ms 26.9% tactic.interactive.simp_core | |
| 28ms 26.9% tactic.interactive.propagate_tags | |
| 28ms 26.9% _interaction._lambda_2 | |
| 28ms 26.9% interaction_monad_orelse | |
| 26ms 25.0% tactic.simplify | |
| 26ms 25.0% tactic.simp_target | |
| 26ms 25.0% tactic.interactive.simp_core_aux._lambda_5 | |
| 26ms 25.0% tactic.interactive.simp_core_aux | |
| 11ms 10.6% tactic.interactive.rintro | |
| 11ms 10.6% tactic.rintro | |
| 9ms 8.7% tactic.rcases_core._main._lambda_2 | |
| 9ms 8.7% tactic.focus1 | |
| 9ms 8.7% tactic.rintro._lambda_3 | |
| 9ms 8.7% tactic.rcases_core._main._lambda_5 | |
| 9ms 8.7% tactic.rcases_core | |
| 9ms 8.7% tactic.rcases.continue | |
| 8ms 7.7% tactic.rcases.continue._main._lambda_2 | |
| 6ms 5.8% tactic.rcases_core._main._lambda_3 | |
| 5ms 4.8% tactic.cases_core | |
| 4ms 3.8% tactic.rcases.process_constructors | |
| 4ms 3.8% tactic.get_arity | |
| 4ms 3.8% tactic.get_pi_arity | |
| 4ms 3.8% tactic.whnf | |
| 3ms 2.9% get_pi_arity_aux | |
| 3ms 2.9% _private.2788053289.get_pi_arity_aux._main._lambda_1 | |
| 2ms 1.9% simp_lemmas.resolve_and_add | |
| 2ms 1.9% tactic.rintro._lambda_2 | |
| 2ms 1.9% tactic.mk_simp_set_core | |
| 2ms 1.9% tactic.mk_simp_set | |
| 2ms 1.9% tactic.intro | |
| 2ms 1.9% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 2ms 1.9% simp_lemmas.append_pexprs | |
| 2ms 1.9% simp_lemmas.add_pexpr | |
| 2ms 1.9% tactic.intro_core | |
| 1ms 1.0% tactic.try | |
| 1ms 1.0% simp_lemmas.add_simp | |
| 1ms 1.0% tactic.try_core | |
| 1ms 1.0% tactic.save_type_info | |
| 1ms 1.0% tactic.save_const_type_info._lambda_1 | |
| 1ms 1.0% cc_state.internalize | |
| elaboration: tactic compilation took 6.6ms | |
| elaboration: tactic compilation took 7.02ms | |
| elaboration: tactic execution took 14ms | |
| num. allocated objects: 109 | |
| num. allocated closures: 113 | |
| 14ms 100.0% _interaction._lambda_2 | |
| 14ms 100.0% tactic.seq | |
| 14ms 100.0% tactic.istep | |
| 14ms 100.0% tactic.interactive.propagate_tags | |
| 14ms 100.0% tactic.step | |
| 14ms 100.0% scope_trace | |
| 14ms 100.0% tactic.istep._lambda_1 | |
| 14ms 100.0% rw_core | |
| 13ms 92.9% interaction_monad.monad._lambda_9 | |
| 13ms 92.9% interactive.loc.apply | |
| 13ms 92.9% tactic.rewrite_core | |
| 13ms 92.9% tactic.rewrite | |
| 13ms 92.9% _private.3132620493.rw_goal._lambda_4 | |
| 13ms 92.9% interaction_monad.orelse' | |
| 13ms 92.9% _private.3132620493.rw_goal._lambda_2 | |
| 13ms 92.9% tactic.rewrite_target | |
| 1ms 7.1% _private.878893113.relation_tactic._lambda_1 | |
| 1ms 7.1% tactic.try | |
| 1ms 7.1% tactic.apply_core | |
| 1ms 7.1% tactic.try_core | |
| 1ms 7.1% relation_tactic | |
| elaboration of prod_mul_distrib took 145ms | |
| elaboration: tactic execution took 71ms | |
| num. allocated objects: 11 | |
| num. allocated closures: 10 | |
| 71ms 100.0% tactic.step | |
| 71ms 100.0% _interaction._lambda_2 | |
| 71ms 100.0% tactic.istep | |
| 71ms 100.0% tactic.cc_core | |
| 71ms 100.0% tactic.istep._lambda_1 | |
| 71ms 100.0% scope_trace | |
| 69ms 97.2% cc_state.mk_using_hs_core | |
| 2ms 2.8% tactic.mk_app | |
| elaboration: tactic execution took 268ms | |
| num. allocated objects: 66 | |
| num. allocated closures: 63 | |
| 268ms 100.0% tactic.to_expr | |
| 268ms 100.0% tactic.step | |
| 268ms 100.0% scope_trace | |
| 268ms 100.0% tactic.istep._lambda_1 | |
| 268ms 100.0% all_goals_core | |
| 268ms 100.0% tactic.istep | |
| 268ms 100.0% tactic.seq | |
| 268ms 100.0% tactic.all_goals | |
| 268ms 100.0% interaction_monad.monad._lambda_9 | |
| 268ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 268ms 100.0% tactic.interactive.exact | |
| elaboration of prod_sigma took 427ms | |
| decl post-processing of prod_mul_distrib took 254ms | |
| parsing took 18.6ms | |
| type checking of prod_comm took 0.175ms | |
| compilation of finset.prod_comm took 0.00227ms | |
| elaboration: tactic compilation took 7.46ms | |
| elaboration: tactic execution took 15ms | |
| num. allocated objects: 133 | |
| num. allocated closures: 119 | |
| 15ms 100.0% tactic.interactive.simp_core | |
| 15ms 100.0% tactic.step | |
| 15ms 100.0% tactic.interactive.propagate_tags | |
| 15ms 100.0% _interaction._lambda_2 | |
| 15ms 100.0% interaction_monad_orelse | |
| 15ms 100.0% tactic.istep | |
| 15ms 100.0% scope_trace | |
| 15ms 100.0% tactic.istep._lambda_1 | |
| 14ms 93.3% tactic.interactive.simp_core_aux._lambda_5 | |
| 14ms 93.3% tactic.interactive.simp_core_aux | |
| 14ms 93.3% tactic.simp_target | |
| 13ms 86.7% tactic.simplify | |
| 1ms 6.7% simp_lemmas.add_pexpr | |
| 1ms 6.7% simp_lemmas.resolve_and_add | |
| 1ms 6.7% tactic.replace_target | |
| 1ms 6.7% simp_lemmas.append_pexprs | |
| 1ms 6.7% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 1ms 6.7% is_valid_simp_lemma_cnst | |
| 1ms 6.7% tactic.mk_simp_set | |
| 1ms 6.7% tactic.mk_eq_mpr | |
| 1ms 6.7% tactic.mk_simp_set_core | |
| elaboration: tactic compilation took 8.1ms | |
| elaboration: tactic execution took 16ms | |
| num. allocated objects: 151 | |
| num. allocated closures: 132 | |
| 16ms 100.0% tactic.interactive.simp_core | |
| 16ms 100.0% tactic.step | |
| 16ms 100.0% tactic.interactive.propagate_tags | |
| 16ms 100.0% _interaction._lambda_2 | |
| 16ms 100.0% scope_trace | |
| 16ms 100.0% tactic.istep | |
| 16ms 100.0% tactic.istep._lambda_1 | |
| 13ms 81.2% tactic.simplify | |
| 13ms 81.2% tactic.interactive.simp_core_aux | |
| 13ms 81.2% tactic.interactive.simp_core_aux._lambda_5 | |
| 13ms 81.2% interaction_monad_orelse | |
| 13ms 81.2% tactic.simp_target | |
| 2ms 12.5% tactic.try_core | |
| 2ms 12.5% tactic.exact | |
| 2ms 12.5% tactic.try | |
| 2ms 12.5% tactic.triv | |
| 1ms 6.2% simp_lemmas.add_pexpr | |
| 1ms 6.2% simp_lemmas.append_pexprs | |
| 1ms 6.2% simp_lemmas.add | |
| 1ms 6.2% tactic.mk_simp_set | |
| 1ms 6.2% tactic.mk_simp_set_core | |
| elaboration of prod_comm took 77.1ms | |
| decl post-processing of prod_comm took 209ms | |
| parsing took 3.37ms | |
| type checking of prod_hom took 0.234ms | |
| compilation of finset.prod_hom took 0.00189ms | |
| decl post-processing of prod_hom took 182ms | |
| parsing took 0.206ms | |
| elaboration: tactic compilation took 7.17ms | |
| elaboration: tactic execution took 1ms | |
| num. allocated objects: 82 | |
| num. allocated closures: 99 | |
| 1ms 100.0% tactic.replace_target | |
| 1ms 100.0% tactic.rewrite_target | |
| 1ms 100.0% _private.3132620493.rw_goal._lambda_2 | |
| 1ms 100.0% interaction_monad.orelse' | |
| 1ms 100.0% _private.3132620493.rw_goal._lambda_4 | |
| 1ms 100.0% scope_trace | |
| 1ms 100.0% rw_core | |
| 1ms 100.0% tactic.exact | |
| 1ms 100.0% tactic.istep._lambda_1 | |
| 1ms 100.0% tactic.step | |
| 1ms 100.0% tactic.interactive.propagate_tags | |
| 1ms 100.0% tactic.istep | |
| 1ms 100.0% tactic.seq | |
| 1ms 100.0% _interaction._lambda_2 | |
| 1ms 100.0% interactive.loc.apply | |
| 1ms 100.0% interaction_monad.monad._lambda_9 | |
| elaboration of prod_hom took 189ms | |
| type checking of sum_nat_cast took 0.367ms | |
| compilation of finset.sum_nat_cast took 0.00189ms | |
| decl post-processing of sum_nat_cast took 0.00302ms | |
| parsing took 42ms | |
| elaboration of sum_nat_cast took 51.1ms | |
| type checking of prod_subset took 0.165ms | |
| compilation of finset.prod_subset took 0.00189ms | |
| elaboration: tactic compilation took 3.67ms | |
| elaboration: tactic compilation took 4.49ms | |
| elaboration: tactic execution took 9ms | |
| num. allocated objects: 184 | |
| num. allocated closures: 180 | |
| 9ms 100.0% _interaction._lambda_2 | |
| 9ms 100.0% scope_trace | |
| 9ms 100.0% tactic.interactive.simpa._lambda_4 | |
| 9ms 100.0% tactic.step | |
| 9ms 100.0% tactic.istep | |
| 9ms 100.0% interaction_monad_orelse | |
| 9ms 100.0% tactic.interactive.simpa._lambda_1 | |
| 9ms 100.0% tactic.istep._lambda_1 | |
| 8ms 88.9% tactic.interactive.simp_core | |
| 8ms 88.9% tactic.try | |
| 8ms 88.9% tactic.try_core | |
| 8ms 88.9% tactic.interactive.propagate_tags | |
| 6ms 66.7% tactic.interactive.simp_core_aux._lambda_5 | |
| 6ms 66.7% tactic.interactive.simp_core_aux | |
| 6ms 66.7% tactic.simp_target | |
| 5ms 55.6% tactic.simplify | |
| 2ms 22.2% simp_lemmas.add_pexpr | |
| 2ms 22.2% simp_lemmas.resolve_and_add | |
| 2ms 22.2% tactic.mk_simp_set_core | |
| 2ms 22.2% tactic.mk_simp_set | |
| 2ms 22.2% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 2ms 22.2% simp_lemmas.append_pexprs | |
| 1ms 11.1% tactic.assumption._lambda_1 | |
| 1ms 11.1% tactic.intro_core | |
| 1ms 11.1% tactic.find_same_type._main._lambda_1 | |
| 1ms 11.1% tactic.find_same_type | |
| 1ms 11.1% tactic.unify | |
| 1ms 11.1% tactic.intro | |
| 1ms 11.1% simp_lemmas.add_simp | |
| 1ms 11.1% is_valid_simp_lemma_cnst | |
| 1ms 11.1% tactic.replace_target | |
| 1ms 11.1% tactic.assert | |
| elaboration: tactic compilation took 7.58ms | |
| elaboration: tactic execution took 18ms | |
| num. allocated objects: 258 | |
| num. allocated closures: 247 | |
| 18ms 100.0% interaction_monad.monad._lambda_9 | |
| 18ms 100.0% scope_trace | |
| 18ms 100.0% tactic.seq | |
| 18ms 100.0% tactic.istep._lambda_1 | |
| 18ms 100.0% tactic.istep | |
| 18ms 100.0% tactic.step | |
| 18ms 100.0% tactic.interactive.propagate_tags | |
| 16ms 88.9% tactic.all_goals | |
| 16ms 88.9% interaction_monad_orelse | |
| 16ms 88.9% _private.3864167971.all_goals_core._main._lambda_2 | |
| 16ms 88.9% all_goals_core | |
| 16ms 88.9% tactic.interactive.simp_core | |
| 15ms 83.3% tactic.simp_target | |
| 15ms 83.3% tactic.interactive.simp_core_aux._lambda_5 | |
| 15ms 83.3% tactic.interactive.simp_core_aux | |
| 14ms 77.8% tactic.simplify | |
| 2ms 11.1% rw_core | |
| 2ms 11.1% _interaction._lambda_2 | |
| 2ms 11.1% interactive.loc.apply | |
| 1ms 5.6% tactic.mk_simp_set_core | |
| 1ms 5.6% simp_lemmas.append_pexprs | |
| 1ms 5.6% tactic.replace_target | |
| 1ms 5.6% tactic.to_expr | |
| 1ms 5.6% tactic.mk_app | |
| 1ms 5.6% simp_lemmas.resolve_and_add | |
| 1ms 5.6% tactic.interactive.to_expr' | |
| 1ms 5.6% _private.3132620493.rw_goal._lambda_2 | |
| 1ms 5.6% interaction_monad.orelse' | |
| 1ms 5.6% _private.3132620493.rw_goal._lambda_4 | |
| 1ms 5.6% tactic.mk_simp_set | |
| 1ms 5.6% simp_lemmas.add_pexpr | |
| 1ms 5.6% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 1ms 5.6% is_valid_simp_lemma_cnst | |
| 1ms 5.6% tactic.mk_id_eq | |
| elaboration: tactic execution took 62ms | |
| num. allocated objects: 31 | |
| num. allocated closures: 39 | |
| 62ms 100.0% tactic.to_expr | |
| 62ms 100.0% tactic.step | |
| 62ms 100.0% scope_trace | |
| 62ms 100.0% tactic.istep._lambda_1 | |
| 62ms 100.0% all_goals_core | |
| 62ms 100.0% tactic.istep | |
| 62ms 100.0% tactic.seq | |
| 62ms 100.0% tactic.all_goals | |
| 62ms 100.0% interaction_monad.monad._lambda_9 | |
| 62ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 62ms 100.0% tactic.interactive.exact | |
| elaboration of prod_subset took 107ms | |
| decl post-processing of prod_subset took 166ms | |
| parsing took 27.4ms | |
| type checking of prod_eq_single took 0.231ms | |
| compilation of finset.prod_eq_single took 0.00227ms | |
| elaboration: tactic compilation took 3.56ms | |
| elaboration: tactic compilation took 12.1ms | |
| elaboration: tactic execution took 10ms | |
| num. allocated objects: 326 | |
| num. allocated closures: 366 | |
| 10ms 100.0% tactic.istep | |
| 10ms 100.0% scope_trace | |
| 10ms 100.0% tactic.istep._lambda_1 | |
| 10ms 100.0% tactic.solve1 | |
| 10ms 100.0% tactic.step | |
| 10ms 100.0% _interaction._lambda_2 | |
| 9ms 90.0% tactic.interactive.propagate_tags | |
| 7ms 70.0% tactic.try_core | |
| 7ms 70.0% interaction_monad_orelse | |
| 7ms 70.0% tactic.try | |
| 6ms 60.0% tactic.interactive.simp_core_aux | |
| 6ms 60.0% tactic.interactive.simpa._lambda_1 | |
| 6ms 60.0% tactic.interactive.simp_core | |
| 6ms 60.0% tactic.interactive.simpa._lambda_2 | |
| 6ms 60.0% tactic.interactive.simpa._lambda_4 | |
| 5ms 50.0% interaction_monad.monad._lambda_9 | |
| 5ms 50.0% tactic.simplify | |
| 4ms 40.0% tactic.interactive.simp_core_aux._lambda_5 | |
| 4ms 40.0% tactic.interactive.rwa | |
| 4ms 40.0% tactic.simp_target | |
| 3ms 30.0% _private.3132620493.rw_goal._lambda_4 | |
| 3ms 30.0% rw_core | |
| 3ms 30.0% interaction_monad.orelse' | |
| 3ms 30.0% _private.3132620493.rw_goal._lambda_2 | |
| 3ms 30.0% interactive.loc.apply | |
| 2ms 20.0% tactic.interactive.simp_core_aux._lambda_2 | |
| 2ms 20.0% tactic.replace_target | |
| 2ms 20.0% tactic.interactive.simp_core_aux._lambda_4 | |
| 2ms 20.0% tactic.to_expr | |
| 2ms 20.0% tactic.interactive.to_expr' | |
| 1ms 10.0% tactic.rewrite_target | |
| 1ms 10.0% tactic.unify | |
| 1ms 10.0% tactic.assert | |
| 1ms 10.0% tactic.find_same_type._main._lambda_1 | |
| 1ms 10.0% tactic.find_same_type | |
| 1ms 10.0% tactic.assert_core | |
| 1ms 10.0% tactic.assumption._lambda_1 | |
| 1ms 10.0% tactic.mk_eq_mpr | |
| elaboration: tactic compilation took 4.6ms | |
| elaboration: tactic execution took 19ms | |
| num. allocated objects: 49 | |
| num. allocated closures: 58 | |
| 19ms 100.0% cc_state.mk_using_hs_core | |
| 19ms 100.0% tactic.step | |
| 19ms 100.0% scope_trace | |
| 19ms 100.0% tactic.istep._lambda_1 | |
| 19ms 100.0% tactic.cc_core | |
| 19ms 100.0% all_goals_core | |
| 19ms 100.0% tactic.istep | |
| 19ms 100.0% tactic.seq | |
| 19ms 100.0% tactic.all_goals | |
| 19ms 100.0% interaction_monad.monad._lambda_9 | |
| 19ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| elaboration: tactic execution took 125ms | |
| num. allocated objects: 31 | |
| num. allocated closures: 40 | |
| 125ms 100.0% tactic.to_expr | |
| 125ms 100.0% tactic.step | |
| 125ms 100.0% scope_trace | |
| 125ms 100.0% tactic.istep._lambda_1 | |
| 125ms 100.0% all_goals_core | |
| 125ms 100.0% tactic.istep | |
| 125ms 100.0% tactic.seq | |
| 125ms 100.0% tactic.all_goals | |
| 125ms 100.0% interaction_monad.monad._lambda_9 | |
| 125ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 125ms 100.0% tactic.interactive.exact | |
| elaboration of prod_eq_single took 205ms | |
| decl post-processing of prod_eq_single took 226ms | |
| parsing took 16.2ms | |
| type checking of prod_attach took 0.175ms | |
| compilation of finset.prod_attach took 0.00189ms | |
| elaboration: tactic compilation took 4.3ms | |
| elaboration: tactic compilation took 4.45ms | |
| elaboration: tactic execution took 16ms | |
| num. allocated objects: 155 | |
| num. allocated closures: 153 | |
| 16ms 100.0% tactic.seq | |
| 16ms 100.0% tactic.step | |
| 16ms 100.0% tactic.istep._lambda_1 | |
| 16ms 100.0% interaction_monad.monad._lambda_9 | |
| 16ms 100.0% scope_trace | |
| 16ms 100.0% tactic.istep | |
| 15ms 93.8% _private.3132620493.rw_goal._lambda_2 | |
| 15ms 93.8% tactic.rewrite_target | |
| 15ms 93.8% _interaction._lambda_2 | |
| 15ms 93.8% interactive.loc.apply | |
| 15ms 93.8% tactic.interactive.propagate_tags | |
| 15ms 93.8% interaction_monad.orelse' | |
| 15ms 93.8% rw_core | |
| 15ms 93.8% _private.3132620493.rw_goal._lambda_4 | |
| 14ms 87.5% tactic.rewrite | |
| 9ms 56.2% tactic.rewrite_core | |
| 5ms 31.2% char.of_nat | |
| 5ms 31.2% tactic.has_opt_auto_param._lambda_2 | |
| 1ms 6.2% tactic.replace_target | |
| 1ms 6.2% tactic.interactive.exact | |
| 1ms 6.2% tactic.all_goals | |
| 1ms 6.2% _private.3864167971.all_goals_core._main._lambda_2 | |
| 1ms 6.2% tactic.mk_id_eq | |
| 1ms 6.2% tactic.mk_app | |
| 1ms 6.2% tactic.exact | |
| 1ms 6.2% all_goals_core | |
| elaboration: tactic compilation took 5.45ms | |
| elaboration: tactic execution took 2ms | |
| num. allocated objects: 108 | |
| num. allocated closures: 107 | |
| 2ms 100.0% tactic.step | |
| 2ms 100.0% tactic.interactive.propagate_tags | |
| 2ms 100.0% _interaction._lambda_2 | |
| 2ms 100.0% tactic.istep | |
| 2ms 100.0% scope_trace | |
| 2ms 100.0% tactic.istep._lambda_1 | |
| 2ms 100.0% rw_core | |
| 1ms 50.0% interaction_monad.monad._lambda_9 | |
| 1ms 50.0% relation_tactic | |
| 1ms 50.0% interactive.loc.apply | |
| 1ms 50.0% _private.3132620493.rw_goal._lambda_4 | |
| 1ms 50.0% tactic.rewrite | |
| 1ms 50.0% _private.878893113.relation_tactic._lambda_1 | |
| 1ms 50.0% interaction_monad.orelse' | |
| 1ms 50.0% tactic.try | |
| 1ms 50.0% _private.3132620493.rw_goal._lambda_2 | |
| 1ms 50.0% tactic.rewrite_target | |
| 1ms 50.0% tactic.apply_core | |
| 1ms 50.0% tactic.rewrite_core | |
| 1ms 50.0% tactic.try_core | |
| elaboration: tactic execution took 40ms | |
| num. allocated objects: 31 | |
| num. allocated closures: 39 | |
| 40ms 100.0% tactic.to_expr | |
| 40ms 100.0% tactic.step | |
| 40ms 100.0% scope_trace | |
| 40ms 100.0% tactic.istep._lambda_1 | |
| 40ms 100.0% all_goals_core | |
| 40ms 100.0% tactic.istep | |
| 40ms 100.0% tactic.seq | |
| 40ms 100.0% tactic.all_goals | |
| 40ms 100.0% interaction_monad.monad._lambda_9 | |
| 40ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 40ms 100.0% tactic.interactive.exact | |
| elaboration of prod_attach took 68.8ms | |
| decl post-processing of prod_attach took 176ms | |
| parsing took 24.9ms | |
| type checking of prod_bij took 0.302ms | |
| compilation of finset.prod_bij took 0.0034ms | |
| elaboration: tactic compilation took 4.78ms | |
| elaboration: tactic compilation took 5.97ms | |
| elaboration: tactic execution took 21ms | |
| num. allocated objects: 664 | |
| num. allocated closures: 578 | |
| 21ms 100.0% scope_trace | |
| 21ms 100.0% tactic.istep._lambda_1 | |
| 21ms 100.0% tactic.step | |
| 21ms 100.0% tactic.seq | |
| 21ms 100.0% tactic.istep | |
| 18ms 85.7% interaction_monad_orelse | |
| 16ms 76.2% tactic.interactive.propagate_tags | |
| 16ms 76.2% tactic.interactive.simp_core | |
| 16ms 76.2% _interaction._lambda_2 | |
| 14ms 66.7% tactic.simplify | |
| 14ms 66.7% tactic.simp_target | |
| 14ms 66.7% tactic.interactive.simp_core_aux | |
| 14ms 66.7% tactic.interactive.simp_core_aux._lambda_5 | |
| 5ms 23.8% all_goals_core | |
| 5ms 23.8% _private.3864167971.all_goals_core._main._lambda_2 | |
| 5ms 23.8% tactic.all_goals | |
| 5ms 23.8% interaction_monad.monad._lambda_9 | |
| 3ms 14.3% tactic.focus1 | |
| 3ms 14.3% tactic.cases_core | |
| 3ms 14.3% tactic.rcases.continue | |
| 3ms 14.3% tactic.rcases_core | |
| 3ms 14.3% tactic.rintro._lambda_3 | |
| 3ms 14.3% tactic.rintro | |
| 3ms 14.3% tactic.rcases_core._main._lambda_2 | |
| 3ms 14.3% tactic.interactive.rintro | |
| 3ms 14.3% tactic.rcases_core._main._lambda_5 | |
| 2ms 9.5% tactic.try_core | |
| 2ms 9.5% simp_lemmas.add_pexpr | |
| 2ms 9.5% list.any_of | |
| 2ms 9.5% simp_lemmas.append_pexprs | |
| 2ms 9.5% simp_lemmas.resolve_and_add | |
| 2ms 9.5% tactic.apply_core | |
| 2ms 9.5% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 2ms 9.5% tactic.mk_simp_set | |
| 2ms 9.5% tactic.apply | |
| 2ms 9.5% tactic.mk_simp_set_core | |
| 2ms 9.5% tactic.solve_by_elim | |
| 2ms 9.5% tactic.apply_assumption._lambda_2 | |
| 2ms 9.5% tactic.solve_by_elim_aux | |
| 2ms 9.5% tactic.apply_assumption._lambda_4 | |
| 1ms 4.8% tactic.rcases.continue._main._lambda_2 | |
| 1ms 4.8% tactic.rcases_core._main._lambda_3 | |
| 1ms 4.8% simp_lemmas.add_simp | |
| 1ms 4.8% is_valid_simp_lemma_cnst | |
| elaboration: tactic compilation took 5.04ms | |
| elaboration: tactic execution took 21ms | |
| num. allocated objects: 255 | |
| num. allocated closures: 174 | |
| 21ms 100.0% tactic.istep | |
| 21ms 100.0% scope_trace | |
| 21ms 100.0% tactic.step | |
| 21ms 100.0% tactic.seq | |
| 21ms 100.0% tactic.istep._lambda_1 | |
| 17ms 81.0% interaction_monad.monad._lambda_9 | |
| 17ms 81.0% tactic.rcases | |
| 17ms 81.0% _interaction._lambda_2 | |
| 17ms 81.0% tactic.interactive.rcases | |
| 16ms 76.2% tactic.rcases_core._main._lambda_5 | |
| 16ms 76.2% tactic.focus1 | |
| 16ms 76.2% tactic.rcases_core | |
| 16ms 76.2% tactic.rcases._lambda_2 | |
| 15ms 71.4% tactic.cases_core | |
| 15ms 71.4% tactic.rcases_core._main._lambda_2 | |
| 13ms 61.9% tactic.rcases.continue | |
| 13ms 61.9% tactic.rcases_core._main._lambda_3 | |
| 4ms 19.0% tactic.interactive.exact | |
| 4ms 19.0% all_goals_core | |
| 4ms 19.0% tactic.all_goals | |
| 4ms 19.0% tactic.to_expr | |
| 4ms 19.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 2ms 9.5% interaction_monad_orelse | |
| 1ms 4.8% tactic.infer_type | |
| 1ms 4.8% tactic.subst_core | |
| 1ms 4.8% tactic.rcases._lambda_1 | |
| elaboration: tactic execution took 71ms | |
| num. allocated objects: 31 | |
| num. allocated closures: 39 | |
| 71ms 100.0% tactic.to_expr | |
| 71ms 100.0% tactic.step | |
| 71ms 100.0% scope_trace | |
| 71ms 100.0% tactic.istep._lambda_1 | |
| 71ms 100.0% all_goals_core | |
| 71ms 100.0% tactic.istep | |
| 71ms 100.0% tactic.seq | |
| 71ms 100.0% tactic.all_goals | |
| 71ms 100.0% interaction_monad.monad._lambda_9 | |
| 71ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 71ms 100.0% tactic.interactive.exact | |
| elaboration of prod_bij took 136ms | |
| decl post-processing of prod_bij took 174ms | |
| parsing took 25.3ms | |
| type checking of prod_bij_ne_one took 0.468ms | |
| compilation of finset.prod_bij_ne_one took 0.00189ms | |
| elaboration: tactic compilation took 4.55ms | |
| elaboration: tactic compilation took 5.31ms | |
| elaboration: tactic execution took 9ms | |
| num. allocated objects: 165 | |
| num. allocated closures: 164 | |
| 9ms 100.0% tactic.seq | |
| 9ms 100.0% tactic.istep | |
| 9ms 100.0% tactic.step | |
| 9ms 100.0% tactic.istep._lambda_1 | |
| 9ms 100.0% scope_trace | |
| 8ms 88.9% tactic.interactive.simp_core | |
| 8ms 88.9% interaction_monad_orelse | |
| 8ms 88.9% _interaction._lambda_2 | |
| 8ms 88.9% tactic.interactive.propagate_tags | |
| 8ms 88.9% tactic.simp_target | |
| 8ms 88.9% tactic.interactive.simp_core_aux | |
| 8ms 88.9% tactic.interactive.simp_core_aux._lambda_5 | |
| 8ms 88.9% tactic.simplify | |
| 1ms 11.1% tactic.to_expr | |
| 1ms 11.1% all_goals_core | |
| 1ms 11.1% interaction_monad.monad._lambda_9 | |
| 1ms 11.1% tactic.all_goals | |
| 1ms 11.1% _private.3864167971.all_goals_core._main._lambda_2 | |
| 1ms 11.1% tactic.interactive.exact | |
| elaboration: tactic compilation took 5.27ms | |
| elaboration: tactic execution took 10ms | |
| num. allocated objects: 127 | |
| num. allocated closures: 124 | |
| 10ms 100.0% tactic.interactive.simp_core_aux._lambda_5 | |
| 10ms 100.0% tactic.interactive.simp_core_aux | |
| 10ms 100.0% tactic.simp_target | |
| 10ms 100.0% scope_trace | |
| 10ms 100.0% tactic.istep._lambda_1 | |
| 10ms 100.0% tactic.step | |
| 10ms 100.0% tactic.interactive.propagate_tags | |
| 10ms 100.0% tactic.istep | |
| 10ms 100.0% tactic.seq | |
| 10ms 100.0% _interaction._lambda_2 | |
| 10ms 100.0% interaction_monad_orelse | |
| 10ms 100.0% tactic.interactive.simp_core | |
| 9ms 90.0% tactic.simplify | |
| 1ms 10.0% tactic.mk_eq_mpr | |
| 1ms 10.0% tactic.replace_target | |
| elaboration: tactic execution took 91ms | |
| num. allocated objects: 31 | |
| num. allocated closures: 39 | |
| 91ms 100.0% tactic.to_expr | |
| 91ms 100.0% tactic.step | |
| 91ms 100.0% scope_trace | |
| 91ms 100.0% tactic.istep._lambda_1 | |
| 91ms 100.0% all_goals_core | |
| 91ms 100.0% tactic.istep | |
| 91ms 100.0% tactic.seq | |
| 91ms 100.0% tactic.all_goals | |
| 91ms 100.0% interaction_monad.monad._lambda_9 | |
| 91ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 91ms 100.0% tactic.interactive.exact | |
| elaboration of prod_bij_ne_one took 159ms | |
| decl post-processing of prod_bij_ne_one took 169ms | |
| parsing took 21.6ms | |
| type checking of exists_ne_one_of_prod_ne_one took 0.154ms | |
| compilation of finset.exists_ne_one_of_prod_ne_one took 0.00189ms | |
| elaboration: tactic compilation took 3.62ms | |
| elaboration: tactic compilation took 5.51ms | |
| elaboration: tactic execution took 13ms | |
| num. allocated objects: 239 | |
| num. allocated closures: 246 | |
| 13ms 100.0% tactic.istep | |
| 13ms 100.0% _interaction._lambda_2 | |
| 13ms 100.0% tactic.step | |
| 13ms 100.0% tactic.istep._lambda_1 | |
| 13ms 100.0% tactic.interactive.rwa | |
| 13ms 100.0% scope_trace | |
| 11ms 84.6% tactic.rewrite_hyp | |
| 11ms 84.6% _private.1542453965.rw_hyp._main._lambda_2 | |
| 11ms 84.6% interaction_monad.orelse' | |
| 11ms 84.6% interaction_monad.monad._lambda_9 | |
| 11ms 84.6% _private.1542453965.rw_hyp._main._lambda_3 | |
| 11ms 84.6% rw_core | |
| 11ms 84.6% tactic.interactive.propagate_tags | |
| 11ms 84.6% interactive.loc.apply | |
| 11ms 84.6% rw_hyp | |
| 9ms 69.2% tactic.rewrite_core | |
| 9ms 69.2% tactic.rewrite | |
| 2ms 15.4% tactic.try | |
| 2ms 15.4% interaction_monad_orelse | |
| 2ms 15.4% tactic.try_core | |
| 2ms 15.4% tactic.replace_hyp | |
| 2ms 15.4% tactic.assumption._lambda_1 | |
| 2ms 15.4% tactic.mk_eq_mp | |
| 2ms 15.4% tactic.find_same_type | |
| 1ms 7.7% tactic.find_same_type._main._lambda_1 | |
| 1ms 7.7% tactic.infer_type | |
| 1ms 7.7% tactic.unify | |
| elaboration: tactic execution took 48ms | |
| num. allocated objects: 31 | |
| num. allocated closures: 39 | |
| 48ms 100.0% tactic.step | |
| 48ms 100.0% scope_trace | |
| 48ms 100.0% tactic.istep._lambda_1 | |
| 48ms 100.0% all_goals_core | |
| 48ms 100.0% tactic.istep | |
| 48ms 100.0% tactic.seq | |
| 48ms 100.0% tactic.all_goals | |
| 48ms 100.0% interaction_monad.monad._lambda_9 | |
| 48ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 48ms 100.0% tactic.interactive.exact | |
| 47ms 97.9% tactic.to_expr | |
| 1ms 2.1% tactic.exact | |
| elaboration of exists_ne_one_of_prod_ne_one took 91.2ms | |
| decl post-processing of exists_ne_one_of_prod_ne_one took 219ms | |
| parsing took 4.06ms | |
| type checking of prod_range_succ took 0.169ms | |
| compilation of finset.prod_range_succ took 0.00264ms | |
| elaboration: tactic compilation took 5.34ms | |
| elaboration: tactic execution took 11ms | |
| num. allocated objects: 95 | |
| num. allocated closures: 107 | |
| 11ms 100.0% interaction_monad.monad._lambda_9 | |
| 11ms 100.0% _private.3132620493.rw_goal._lambda_2 | |
| 11ms 100.0% interaction_monad.orelse' | |
| 11ms 100.0% scope_trace | |
| 11ms 100.0% rw_core | |
| 11ms 100.0% interactive.loc.apply | |
| 11ms 100.0% tactic.istep._lambda_1 | |
| 11ms 100.0% tactic.istep | |
| 11ms 100.0% _private.3132620493.rw_goal._lambda_4 | |
| 11ms 100.0% _interaction._lambda_2 | |
| 11ms 100.0% tactic.interactive.propagate_tags | |
| 11ms 100.0% tactic.step | |
| 10ms 90.9% tactic.to_expr | |
| 10ms 90.9% tactic.interactive.to_expr' | |
| 1ms 9.1% tactic.rewrite | |
| 1ms 9.1% tactic.rewrite_core | |
| 1ms 9.1% tactic.rewrite_target | |
| elaboration of prod_range_succ took 29.1ms | |
| decl post-processing of prod_range_succ took 160ms | |
| parsing took 4.39ms | |
| type checking of prod_range_succ' took 0.16ms | |
| compilation of finset.prod_range_succ' took 0.00189ms | |
| decl post-processing of prod_range_succ' took 0.00264ms | |
| parsing took 11.2ms | |
| type checking of prod_const took 0.168ms | |
| compilation of finset.prod_const took 0.00227ms | |
| decl post-processing of prod_const took 0.427ms | |
| parsing took 0.27ms | |
| type checking of sum_const took 0.15ms | |
| compilation of finset.sum_const took 0.00189ms | |
| decl post-processing of sum_const took 0.402ms | |
| elaboration: tactic compilation took 7.52ms | |
| elaboration of sum_const took 7.08ms | |
| elaboration: tactic compilation took 8.08ms | |
| elaboration: tactic execution took 12ms | |
| num. allocated objects: 192 | |
| num. allocated closures: 173 | |
| 12ms 100.0% interaction_monad.monad._lambda_9 | |
| 12ms 100.0% interactive.loc.apply | |
| 12ms 100.0% tactic.rewrite_target | |
| 12ms 100.0% _private.3132620493.rw_goal._lambda_2 | |
| 12ms 100.0% interaction_monad.orelse' | |
| 12ms 100.0% scope_trace | |
| 12ms 100.0% rw_core | |
| 12ms 100.0% tactic.step | |
| 12ms 100.0% tactic.istep._lambda_1 | |
| 12ms 100.0% tactic.istep | |
| 12ms 100.0% _private.3132620493.rw_goal._lambda_4 | |
| 12ms 100.0% _interaction._lambda_2 | |
| 12ms 100.0% tactic.interactive.propagate_tags | |
| 8ms 66.7% tactic.rewrite | |
| 8ms 66.7% tactic.rewrite_core | |
| 4ms 33.3% tactic.mk_eq_mpr | |
| 4ms 33.3% tactic.replace_target | |
| elaboration of prod_const took 39.5ms | |
| elaboration: tactic execution took 11ms | |
| num. allocated objects: 239 | |
| num. allocated closures: 216 | |
| 11ms 100.0% tactic.seq | |
| 11ms 100.0% tactic.istep._lambda_1 | |
| 11ms 100.0% tactic.istep | |
| 11ms 100.0% scope_trace | |
| 11ms 100.0% interaction_monad.monad._lambda_9 | |
| 11ms 100.0% tactic.step | |
| 10ms 90.9% tactic.rewrite | |
| 10ms 90.9% interactive.loc.apply | |
| 10ms 90.9% tactic.rewrite_target | |
| 10ms 90.9% _private.3132620493.rw_goal._lambda_2 | |
| 10ms 90.9% interaction_monad.orelse' | |
| 10ms 90.9% _interaction._lambda_2 | |
| 10ms 90.9% _private.3132620493.rw_goal._lambda_4 | |
| 10ms 90.9% tactic.interactive.propagate_tags | |
| 10ms 90.9% rw_core | |
| 9ms 81.8% tactic.rewrite_core | |
| 1ms 9.1% tactic.interactive.exact | |
| 1ms 9.1% all_goals_core | |
| 1ms 9.1% tactic.to_expr | |
| 1ms 9.1% tactic.has_opt_auto_param._lambda_2 | |
| 1ms 9.1% tactic.all_goals | |
| 1ms 9.1% char.of_nat | |
| 1ms 9.1% _private.3864167971.all_goals_core._main._lambda_2 | |
| elaboration of prod_range_succ' took 102ms | |
| parsing took 0.213ms | |
| type checking of sum_range_succ' took 0.141ms | |
| compilation of finset.sum_range_succ' took 0.00151ms | |
| decl post-processing of sum_range_succ' took 0.00264ms | |
| elaboration of sum_range_succ' took 3.46ms | |
| parsing took 0.133ms | |
| type checking of prod_inv_distrib took 0.121ms | |
| compilation of finset.prod_inv_distrib took 0.00189ms | |
| elaboration of prod_inv_distrib took 6.26ms | |
| decl post-processing of prod_inv_distrib took 157ms | |
| parsing took 0.28ms | |
| type checking of card_sigma took 0.177ms | |
| compilation of finset.card_sigma took 0.00151ms | |
| decl post-processing of card_sigma took 0.215ms | |
| parsing took 0.157ms | |
| elaboration of card_sigma took 5.47ms | |
| type checking of sum_sub_distrib took 0.136ms | |
| compilation of finset.sum_sub_distrib took 0.00151ms | |
| decl post-processing of sum_sub_distrib took 0.35ms | |
| elaboration of sum_sub_distrib took 12.4ms | |
| parsing took 12.6ms | |
| type checking of sum_le_sum took 0.179ms | |
| compilation of finset.sum_le_sum took 0.00189ms | |
| decl post-processing of sum_le_sum took 0.00264ms | |
| parsing took 2ms | |
| elaboration: tactic compilation took 8.2ms | |
| type checking of zero_le_sum took 0.498ms | |
| compilation of finset.zero_le_sum took 0.00302ms | |
| decl post-processing of zero_le_sum took 0.0117ms | |
| parsing took 4.32ms | |
| elaboration: tactic compilation took 7.01ms | |
| elaboration: tactic execution took 11ms | |
| num. allocated objects: 69 | |
| num. allocated closures: 86 | |
| 11ms 100.0% tactic.interactive.simpa._lambda_2 | |
| 11ms 100.0% _interaction._lambda_2 | |
| 11ms 100.0% scope_trace | |
| 11ms 100.0% tactic.interactive.simp_core | |
| 11ms 100.0% tactic.try | |
| 11ms 100.0% tactic.istep._lambda_1 | |
| 11ms 100.0% tactic.interactive.propagate_tags | |
| 11ms 100.0% tactic.interactive.simpa._lambda_1 | |
| 11ms 100.0% tactic.istep | |
| 11ms 100.0% interaction_monad_orelse | |
| 11ms 100.0% tactic.try_core | |
| 11ms 100.0% tactic.step | |
| 11ms 100.0% tactic.interactive.simpa._lambda_4 | |
| 10ms 90.9% tactic.simplify | |
| 10ms 90.9% tactic.interactive.simp_core_aux | |
| 8ms 72.7% tactic.interactive.simp_core_aux._lambda_2 | |
| 8ms 72.7% tactic.interactive.simp_core_aux._lambda_4 | |
| 8ms 72.7% interaction_monad.monad._lambda_9 | |
| 2ms 18.2% tactic.interactive.simp_core_aux._lambda_5 | |
| 2ms 18.2% tactic.simp_target | |
| 1ms 9.1% simp_lemmas.append_pexprs | |
| 1ms 9.1% tactic.to_expr | |
| 1ms 9.1% tactic.mk_simp_set | |
| 1ms 9.1% tactic.mk_simp_set_core | |
| 1ms 9.1% simp_lemmas.add_pexpr | |
| elaboration of sum_le_sum took 80.5ms | |
| elaboration: tactic execution took 0ms | |
| elaboration of zero_le_sum took 37.9ms | |
| type checking of sum_le_zero took 0.466ms | |
| compilation of finset.sum_le_zero took 0.00415ms | |
| decl post-processing of sum_le_zero took 0.00415ms | |
| parsing took 0.321ms | |
| elaboration: tactic compilation took 8.49ms | |
| elaboration: tactic execution took 0ms | |
| elaboration of sum_le_zero took 27.3ms | |
| type checking of sum_mul took 0.204ms | |
| compilation of finset.sum_mul took 0.00264ms | |
| decl post-processing of sum_mul took 0.00302ms | |
| parsing took 0.298ms | |
| type checking of mul_sum took 0.177ms | |
| compilation of finset.mul_sum took 0.00227ms | |
| decl post-processing of mul_sum took 0.00378ms | |
| elaboration of sum_mul took 18.9ms | |
| parsing took 7.93ms | |
| elaboration of mul_sum took 27.8ms | |
| type checking of prod_eq_zero took 0.75ms | |
| compilation of finset.prod_eq_zero took 0.00831ms | |
| decl post-processing of prod_eq_zero took 0.00906ms | |
| elaboration: tactic compilation took 7.57ms | |
| elaboration: tactic execution took 0ms | |
| elaboration: tactic compilation took 15.4ms | |
| elaboration: tactic execution took 0ms | |
| elaboration of prod_eq_zero took 115ms | |
| parsing took 344ms | |
| type checking of prod_sum took 0.534ms | |
| compilation of finset.prod_sum took 0.00264ms | |
| decl post-processing of prod_sum took 0.00302ms | |
| parsing took 13.3ms | |
| type checking of prod_eq_zero_iff took 0.314ms | |
| compilation of finset.prod_eq_zero_iff took 0.00302ms | |
| decl post-processing of prod_eq_zero_iff took 0.0034ms | |
| parsing took 13.9ms | |
| type checking of sum_le_sum' took 0.241ms | |
| compilation of finset.sum_le_sum' took 0.0068ms | |
| decl post-processing of sum_le_sum' took 0.0034ms | |
| parsing took 2.99ms | |
| elaboration: tactic compilation took 11.4ms | |
| elaboration: tactic compilation took 5.88ms | |
| elaboration: tactic execution took 5ms | |
| num. allocated objects: 452 | |
| num. allocated closures: 415 | |
| 5ms 100.0% _private.878893113.relation_tactic._lambda_1 | |
| 5ms 100.0% scope_trace | |
| 5ms 100.0% tactic.try | |
| 5ms 100.0% tactic.istep._lambda_1 | |
| 5ms 100.0% tactic.try_core | |
| 5ms 100.0% tactic.istep | |
| 5ms 100.0% _interaction._lambda_2 | |
| 5ms 100.0% tactic.interactive.propagate_tags | |
| 5ms 100.0% tactic.step | |
| 5ms 100.0% relation_tactic | |
| 5ms 100.0% tactic.apply_core | |
| 5ms 100.0% tactic.interactive.simp_core | |
| elaboration of prod_eq_zero_iff took 69ms | |
| type checking of zero_le_sum' took 0.282ms | |
| compilation of finset.zero_le_sum' took 0.00302ms | |
| decl post-processing of zero_le_sum' took 0.00302ms | |
| elaboration: tactic compilation took 40.8ms | |
| parsing took 2.98ms | |
| elaboration: tactic execution took 11ms | |
| num. allocated objects: 69 | |
| num. allocated closures: 86 | |
| 11ms 100.0% _interaction._lambda_2 | |
| 11ms 100.0% tactic.interactive.simpa._lambda_1 | |
| 11ms 100.0% tactic.try_core | |
| 11ms 100.0% tactic.interactive.simpa._lambda_2 | |
| 11ms 100.0% tactic.interactive.simpa._lambda_4 | |
| 11ms 100.0% tactic.istep | |
| 11ms 100.0% tactic.step | |
| 11ms 100.0% tactic.interactive.propagate_tags | |
| 11ms 100.0% interaction_monad_orelse | |
| 11ms 100.0% tactic.simplify | |
| 11ms 100.0% tactic.istep._lambda_1 | |
| 11ms 100.0% tactic.try | |
| 11ms 100.0% scope_trace | |
| 11ms 100.0% tactic.simp_target | |
| 11ms 100.0% tactic.interactive.simp_core | |
| 11ms 100.0% tactic.interactive.simp_core_aux | |
| 11ms 100.0% tactic.interactive.simp_core_aux._lambda_5 | |
| elaboration of sum_le_sum' took 65.3ms | |
| elaboration: tactic compilation took 6.79ms | |
| elaboration: tactic execution took 0ms | |
| elaboration of zero_le_sum' took 17.8ms | |
| type checking of sum_le_zero' took 0.268ms | |
| compilation of finset.sum_le_zero' took 0.00227ms | |
| decl post-processing of sum_le_zero' took 0.0034ms | |
| elaboration: tactic compilation took 5.15ms | |
| elaboration: tactic execution took 2ms | |
| num. allocated objects: 113 | |
| num. allocated closures: 110 | |
| 2ms 100.0% tactic.apply_core | |
| 2ms 100.0% scope_trace | |
| 2ms 100.0% _private.878893113.relation_tactic._lambda_1 | |
| 2ms 100.0% rw_core | |
| 2ms 100.0% tactic.try | |
| 2ms 100.0% tactic.istep._lambda_1 | |
| 2ms 100.0% tactic.try_core | |
| 2ms 100.0% tactic.istep | |
| 2ms 100.0% _interaction._lambda_2 | |
| 2ms 100.0% tactic.interactive.propagate_tags | |
| 2ms 100.0% tactic.step | |
| 2ms 100.0% relation_tactic | |
| elaboration of sum_le_zero' took 15.8ms | |
| parsing took 21.6ms | |
| type checking of sum_le_sum_of_subset_of_nonneg took 0.416ms | |
| compilation of finset.sum_le_sum_of_subset_of_nonneg took 0.00189ms | |
| decl post-processing of sum_le_sum_of_subset_of_nonneg took 0.00302ms | |
| parsing took 13.5ms | |
| elaboration: tactic compilation took 6.46ms | |
| elaboration: tactic execution took 7ms | |
| num. allocated objects: 203 | |
| num. allocated closures: 186 | |
| 7ms 100.0% tactic.interactive.simpa._lambda_4 | |
| 7ms 100.0% tactic.step | |
| 7ms 100.0% tactic.interactive.simpa._lambda_1 | |
| 7ms 100.0% _interaction._lambda_2 | |
| 7ms 100.0% tactic.istep._lambda_1 | |
| 7ms 100.0% scope_trace | |
| 7ms 100.0% tactic.istep | |
| 7ms 100.0% interaction_monad_orelse | |
| 4ms 57.1% tactic.interactive.propagate_tags | |
| 4ms 57.1% tactic.try | |
| 4ms 57.1% tactic.try_core | |
| 4ms 57.1% tactic.interactive.simp_core | |
| 3ms 42.9% tactic.interactive.simp_core_aux._lambda_5 | |
| 3ms 42.9% tactic.simplify | |
| 3ms 42.9% tactic.assumption._lambda_1 | |
| 3ms 42.9% tactic.interactive.simp_core_aux | |
| 3ms 42.9% tactic.simp_target | |
| 2ms 28.6% tactic.find_same_type | |
| 2ms 28.6% tactic.infer_type | |
| 1ms 14.3% tactic.mk_simp_set_core | |
| 1ms 14.3% tactic.mk_simp_set | |
| 1ms 14.3% simp_lemmas.append_pexprs | |
| 1ms 14.3% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 1ms 14.3% simp_lemmas.resolve_and_add | |
| 1ms 14.3% tactic.exact | |
| 1ms 14.3% simp_lemmas.add_simp | |
| 1ms 14.3% simp_lemmas.add_pexpr | |
| elaboration: tactic compilation took 6.5ms | |
| elaboration: tactic execution took 1ms | |
| num. allocated objects: 33 | |
| num. allocated closures: 67 | |
| 1ms 100.0% tactic.to_expr | |
| 1ms 100.0% tactic.interactive.to_expr' | |
| 1ms 100.0% _private.3132620493.rw_goal._lambda_2 | |
| 1ms 100.0% interaction_monad.orelse' | |
| 1ms 100.0% scope_trace | |
| 1ms 100.0% rw_core | |
| 1ms 100.0% tactic.istep._lambda_1 | |
| 1ms 100.0% tactic.istep | |
| 1ms 100.0% _private.3132620493.rw_goal._lambda_4 | |
| 1ms 100.0% _interaction._lambda_2 | |
| 1ms 100.0% tactic.interactive.propagate_tags | |
| 1ms 100.0% tactic.step | |
| 1ms 100.0% interactive.loc.apply | |
| 1ms 100.0% interaction_monad.monad._lambda_9 | |
| elaboration of sum_le_sum_of_subset_of_nonneg took 61.8ms | |
| type checking of sum_eq_zero_iff_of_nonneg took 0.403ms | |
| compilation of finset.sum_eq_zero_iff_of_nonneg took 0.00264ms | |
| decl post-processing of sum_eq_zero_iff_of_nonneg took 0.0034ms | |
| parsing took 4.41ms | |
| type checking of single_le_sum took 0.287ms | |
| compilation of finset.single_le_sum took 0.00227ms | |
| decl post-processing of single_le_sum took 0.0034ms | |
| parsing took 0.213ms | |
| elaboration: tactic compilation took 6.45ms | |
| type checking of sum_le_sum_of_subset took 0.249ms | |
| compilation of finset.sum_le_sum_of_subset took 0.00189ms | |
| decl post-processing of sum_le_sum_of_subset took 0.0034ms | |
| elaboration: tactic execution took 0ms | |
| elaboration of single_le_sum took 22.3ms | |
| elaboration: tactic compilation took 12.2ms | |
| elaboration of sum_le_sum_of_subset took 7.11ms | |
| parsing took 25.7ms | |
| elaboration: tactic execution took 38ms | |
| num. allocated objects: 2744 | |
| num. allocated closures: 1511 | |
| 38ms 100.0% tactic.istep._lambda_1 | |
| 38ms 100.0% tactic.seq | |
| 38ms 100.0% tactic.istep | |
| 38ms 100.0% interaction_monad.monad._lambda_9 | |
| 38ms 100.0% scope_trace | |
| 38ms 100.0% tactic.step | |
| 34ms 89.5% tactic.all_goals | |
| 34ms 89.5% _private.3864167971.all_goals_core._main._lambda_2 | |
| 34ms 89.5% all_goals_core | |
| 32ms 84.2% interaction_monad_orelse | |
| 23ms 60.5% tactic.solve_by_elim | |
| 23ms 60.5% tactic.solve_by_elim_aux | |
| 23ms 60.5% tactic.apply_assumption._lambda_4 | |
| 23ms 60.5% tactic.try_core | |
| 23ms 60.5% list.any_of | |
| 22ms 57.9% tactic.apply_core | |
| 22ms 57.9% tactic.apply_assumption._lambda_2 | |
| 15ms 39.5% tactic.apply | |
| 14ms 36.8% tactic.symm_apply._lambda_1 | |
| 11ms 28.9% tactic.interactive.propagate_tags | |
| 7ms 18.4% tactic.interactive.simp_core_aux._lambda_5 | |
| 7ms 18.4% tactic.interactive.simp_core_aux | |
| 7ms 18.4% _private.878893113.relation_tactic._lambda_1 | |
| 7ms 18.4% tactic.simp_target | |
| 7ms 18.4% tactic.simplify | |
| 7ms 18.4% relation_tactic | |
| 7ms 18.4% tactic.interactive.simp_core | |
| 4ms 10.5% _private.3132620493.rw_goal._lambda_4 | |
| 4ms 10.5% interactive.loc.apply | |
| 4ms 10.5% _interaction._lambda_2 | |
| 4ms 10.5% _private.3132620493.rw_goal._lambda_2 | |
| 4ms 10.5% interaction_monad.orelse' | |
| 4ms 10.5% rw_core | |
| 3ms 7.9% tactic.focus1 | |
| 3ms 7.9% tactic.rintro | |
| 3ms 7.9% tactic.interactive.rintro | |
| 2ms 5.3% tactic.rcases.continue._main._lambda_2 | |
| 2ms 5.3% tactic.rewrite_target | |
| 2ms 5.3% tactic.rcases_core._main._lambda_3 | |
| 2ms 5.3% tactic.rintro._lambda_3 | |
| 2ms 5.3% tactic.rcases.continue | |
| 2ms 5.3% tactic.subst_core | |
| 2ms 5.3% tactic.rcases_core | |
| 2ms 5.3% tactic.rcases_core._main._lambda_5 | |
| 2ms 5.3% tactic.replace_target | |
| 2ms 5.3% tactic.interactive.to_expr' | |
| 2ms 5.3% tactic.to_expr | |
| 2ms 5.3% tactic.mk_eq_mpr | |
| 1ms 2.6% tactic.cases | |
| 1ms 2.6% tactic.intro_core | |
| 1ms 2.6% tactic.rintro._lambda_2 | |
| 1ms 2.6% tactic.interactive.cases_core._lambda_1 | |
| 1ms 2.6% tactic.intro | |
| 1ms 2.6% tactic.interactive.cases_core | |
| 1ms 2.6% tactic.kdependencies | |
| 1ms 2.6% kdependencies_core | |
| 1ms 2.6% tactic.interactive.cases | |
| 1ms 2.6% tactic.kdepends_on | |
| 1ms 2.6% tactic.revert_kdependencies | |
| type checking of sum_le_sum_of_ne_zero took 0.48ms | |
| compilation of finset.sum_le_sum_of_ne_zero took 0.00227ms | |
| decl post-processing of sum_le_sum_of_ne_zero took 0.0034ms | |
| elaboration of sum_eq_zero_iff_of_nonneg took 117ms | |
| parsing took 6.96ms | |
| type checking of abs_sum_le_sum_abs took 0.291ms | |
| compilation of finset.abs_sum_le_sum_abs took 0.00189ms | |
| decl post-processing of abs_sum_le_sum_abs took 0.00302ms | |
| parsing took 0.562ms | |
| type checking of card_pi took 0.37ms | |
| compilation of finset.card_pi took 0.00227ms | |
| decl post-processing of card_pi took 0.472ms | |
| elaboration: tactic compilation took 6.93ms | |
| elaboration of card_pi took 38ms | |
| elaboration: tactic execution took 0ms | |
| elaboration: tactic compilation took 7.6ms | |
| elaboration: tactic execution took 0ms | |
| elaboration of abs_sum_le_sum_abs took 91.8ms | |
| parsing took 25.8ms | |
| elaboration: tactic compilation took 7.29ms | |
| elaboration: tactic execution took 7ms | |
| num. allocated objects: 232 | |
| num. allocated closures: 211 | |
| 7ms 100.0% tactic.seq | |
| 7ms 100.0% tactic.step | |
| 7ms 100.0% tactic.istep._lambda_1 | |
| 7ms 100.0% tactic.istep | |
| 7ms 100.0% scope_trace | |
| 7ms 100.0% interaction_monad.monad._lambda_9 | |
| 6ms 85.7% rw_core | |
| 6ms 85.7% interactive.loc.apply | |
| 6ms 85.7% tactic.rewrite_target | |
| 6ms 85.7% _private.3132620493.rw_goal._lambda_2 | |
| 6ms 85.7% interaction_monad.orelse' | |
| 6ms 85.7% _private.3132620493.rw_goal._lambda_4 | |
| 6ms 85.7% _interaction._lambda_2 | |
| 6ms 85.7% tactic.interactive.propagate_tags | |
| 4ms 57.1% tactic.rewrite | |
| 4ms 57.1% tactic.rewrite_core | |
| 2ms 28.6% tactic.replace_target | |
| 1ms 14.3% _private.3864167971.all_goals_core._main._lambda_2 | |
| 1ms 14.3% tactic.all_goals | |
| 1ms 14.3% tactic.interactive.concat_tags._lambda_5 | |
| 1ms 14.3% tactic.apply | |
| 1ms 14.3% tactic.apply_core | |
| 1ms 14.3% tactic.exact | |
| 1ms 14.3% all_goals_core | |
| 1ms 14.3% tactic.interactive.apply._lambda_1 | |
| elaboration: tactic compilation took 7.69ms | |
| elaboration: tactic execution took 23ms | |
| num. allocated objects: 166 | |
| num. allocated closures: 164 | |
| 23ms 100.0% tactic.seq | |
| 23ms 100.0% tactic.istep | |
| 23ms 100.0% tactic.step | |
| 23ms 100.0% tactic.istep._lambda_1 | |
| 23ms 100.0% scope_trace | |
| 19ms 82.6% tactic.interactive.simp_core | |
| 19ms 82.6% _interaction._lambda_2 | |
| 19ms 82.6% tactic.interactive.propagate_tags | |
| 17ms 73.9% tactic.simp_target | |
| 17ms 73.9% tactic.interactive.simp_core_aux | |
| 17ms 73.9% tactic.interactive.simp_core_aux._lambda_5 | |
| 17ms 73.9% tactic.simplify | |
| 17ms 73.9% interaction_monad_orelse | |
| 4ms 17.4% tactic.to_expr | |
| 4ms 17.4% all_goals_core | |
| 4ms 17.4% interaction_monad.monad._lambda_9 | |
| 4ms 17.4% _private.3864167971.all_goals_core._main._lambda_2 | |
| 4ms 17.4% tactic.all_goals | |
| 4ms 17.4% tactic.interactive.exact | |
| elaboration: tactic compilation took 10.6ms | |
| elaboration: tactic execution took 13ms | |
| num. allocated objects: 201 | |
| num. allocated closures: 196 | |
| 13ms 100.0% tactic.interactive.simpa._lambda_1 | |
| 13ms 100.0% tactic.interactive.simpa._lambda_4 | |
| 13ms 100.0% tactic.istep | |
| 13ms 100.0% tactic.step | |
| 13ms 100.0% interaction_monad_orelse | |
| 13ms 100.0% _interaction._lambda_2 | |
| 13ms 100.0% scope_trace | |
| 13ms 100.0% tactic.istep._lambda_1 | |
| 12ms 92.3% tactic.try | |
| 12ms 92.3% tactic.try_core | |
| 12ms 92.3% tactic.interactive.propagate_tags | |
| 12ms 92.3% tactic.simp_target | |
| 12ms 92.3% tactic.interactive.simp_core | |
| 12ms 92.3% tactic.interactive.simp_core_aux | |
| 12ms 92.3% tactic.interactive.simp_core_aux._lambda_5 | |
| 12ms 92.3% tactic.simplify | |
| 1ms 7.7% tactic.unify | |
| 1ms 7.7% tactic.find_same_type | |
| 1ms 7.7% tactic.assumption._lambda_1 | |
| 1ms 7.7% tactic.find_same_type._main._lambda_1 | |
| elaboration of sum_le_sum_of_ne_zero took 237ms | |
| type checking of is_group_hom.prod took 0.329ms | |
| compilation of is_group_hom.prod took 0.00264ms | |
| decl post-processing of is_group_hom.prod took 0.00264ms | |
| elaboration: tactic compilation took 8.57ms | |
| parsing took 32ms | |
| elaboration: tactic execution took 84ms | |
| num. allocated objects: 540 | |
| num. allocated closures: 528 | |
| 84ms 100.0% tactic.istep._lambda_1 | |
| 84ms 100.0% all_goals_core | |
| 84ms 100.0% scope_trace | |
| 84ms 100.0% tactic.step | |
| 84ms 100.0% interaction_monad.monad._lambda_9 | |
| 84ms 100.0% tactic.interactive.propagate_tags | |
| 84ms 100.0% tactic.istep | |
| 84ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| 84ms 100.0% tactic.seq | |
| 84ms 100.0% tactic.all_goals | |
| 83ms 98.8% tactic.focus1 | |
| 83ms 98.8% tactic.interactive.simp_core | |
| 83ms 98.8% tactic.interactive.propagate_tags._lambda_3 | |
| 81ms 96.4% interaction_monad_orelse | |
| 77ms 91.7% tactic.simplify | |
| 77ms 91.7% tactic.simp_target | |
| 77ms 91.7% tactic.interactive.simp_core_aux._lambda_5 | |
| 77ms 91.7% tactic.interactive.simp_core_aux | |
| 6ms 7.1% tactic.mk_simp_set_core | |
| 6ms 7.1% tactic.mk_simp_set | |
| 5ms 6.0% simp_lemmas.append_pexprs | |
| 5ms 6.0% simp_lemmas.add_pexpr | |
| 4ms 4.8% simp_lemmas.resolve_and_add | |
| 3ms 3.6% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 2ms 2.4% tactic.try_core | |
| 2ms 2.4% tactic.try | |
| 2ms 2.4% tactic.save_type_info | |
| 2ms 2.4% simp_lemmas.add_simp | |
| 2ms 2.4% tactic.save_const_type_info._lambda_1 | |
| 1ms 1.2% tactic.get_main_tag | |
| 1ms 1.2% add_simps | |
| 1ms 1.2% simp_lemmas.add | |
| 1ms 1.2% tactic.main_goal | |
| 1ms 1.2% tactic.to_expr | |
| 1ms 1.2% tactic.get_goals | |
| 1ms 1.2% _private.4232751329.simp_lemmas.resolve_and_add._lambda_3 | |
| elaboration of is_group_hom.prod took 118ms | |
| type checking of is_group_anti_hom.prod took 0.309ms | |
| compilation of is_group_anti_hom.prod took 0.00227ms | |
| decl post-processing of is_group_anti_hom.prod took 0.00302ms | |
| parsing took 0.234ms | |
| elaboration: tactic compilation took 7.1ms | |
| elaboration: tactic execution took 33ms | |
| num. allocated objects: 465 | |
| num. allocated closures: 425 | |
| 33ms 100.0% tactic.step | |
| 33ms 100.0% _private.3954514829.focus_aux._main._lambda_3 | |
| 33ms 100.0% interaction_monad.monad._lambda_9 | |
| 33ms 100.0% tactic.interactive.simp_core_aux._lambda_5 | |
| 33ms 100.0% focus_aux | |
| 33ms 100.0% tactic.seq_focus | |
| 33ms 100.0% tactic.interactive.simp_core_aux | |
| 33ms 100.0% tactic.istep | |
| 33ms 100.0% tactic.interactive.propagate_tags | |
| 33ms 100.0% tactic.focus | |
| 33ms 100.0% tactic.istep._lambda_1 | |
| 33ms 100.0% tactic.focus1 | |
| 33ms 100.0% scope_trace | |
| 33ms 100.0% tactic.simp_target | |
| 33ms 100.0% tactic.interactive.propagate_tags._lambda_3 | |
| 33ms 100.0% tactic.interactive.simp_core | |
| 33ms 100.0% interaction_monad_orelse | |
| 32ms 97.0% tactic.simplify | |
| 1ms 3.0% tactic.mk_eq_mpr | |
| 1ms 3.0% tactic.replace_target | |
| elaboration of is_group_anti_hom.prod took 75.6ms | |
| type checking of inv_prod took 0.239ms | |
| compilation of inv_prod took 0.00227ms | |
| decl post-processing of inv_prod took 0.00302ms | |
| elaboration of inv_prod took 1.18ms | |
| parsing took 98.8ms | |
| type checking of to_finset_sum_count_eq took 0.185ms | |
| compilation of multiset.to_finset_sum_count_eq took 0.00189ms | |
| decl post-processing of to_finset_sum_count_eq took 0.289ms | |
| elaboration: tactic compilation took 4.99ms | |
| elaboration: tactic execution took 28ms | |
| num. allocated objects: 787 | |
| num. allocated closures: 741 | |
| 28ms 100.0% tactic.seq_focus | |
| 28ms 100.0% tactic.step | |
| 28ms 100.0% tactic.istep | |
| 28ms 100.0% scope_trace | |
| 28ms 100.0% interaction_monad.monad._lambda_9 | |
| 28ms 100.0% tactic.istep._lambda_1 | |
| 23ms 82.1% tactic.simp_target | |
| 20ms 71.4% tactic.simplify | |
| 18ms 64.3% interaction_monad_orelse | |
| 17ms 60.7% tactic.interactive.simp_core | |
| 17ms 60.7% _private.3954514829.focus_aux._main._lambda_3 | |
| 17ms 60.7% focus_aux | |
| 17ms 60.7% tactic.interactive.propagate_tags | |
| 17ms 60.7% tactic.focus | |
| 13ms 46.4% tactic.interactive.simp_core_aux._lambda_5 | |
| 13ms 46.4% tactic.interactive.simp_core_aux | |
| 11ms 39.3% _private.3864167971.all_goals_core._main._lambda_2 | |
| 11ms 39.3% _interaction._lambda_2 | |
| 11ms 39.3% tactic.reduce_ifs_at | |
| 11ms 39.3% tactic.seq | |
| 11ms 39.3% tactic.all_goals | |
| 11ms 39.3% all_goals_core | |
| 11ms 39.3% tactic.using_new_ref | |
| 11ms 39.3% split_ifs_core | |
| 11ms 39.3% _private.3909137105.split_ifs_core._main._lambda_1 | |
| 10ms 35.7% tactic.reduce_ifs_at._lambda_4 | |
| 4ms 14.3% simp_lemmas.resolve_and_add | |
| 4ms 14.3% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 4ms 14.3% simp_lemmas.add_pexpr | |
| 4ms 14.3% tactic.mk_simp_set | |
| 4ms 14.3% tactic.mk_simp_set_core | |
| 4ms 14.3% simp_lemmas.append_pexprs | |
| 3ms 10.7% tactic.replace_target | |
| 2ms 7.1% is_valid_simp_lemma_cnst | |
| 2ms 7.1% simp_lemmas.add_simp | |
| 1ms 3.6% tactic.unify | |
| 1ms 3.6% tactic.eval_expr | |
| 1ms 3.6% tactic.assumption._lambda_1 | |
| 1ms 3.6% tactic.get_user_simp_lemmas | |
| 1ms 3.6% tactic.find_same_type._main._lambda_1 | |
| 1ms 3.6% get_attribute_cache_dyn._lambda_1 | |
| 1ms 3.6% tactic.exact | |
| 1ms 3.6% tactic.find_same_type | |
| elaboration: tactic compilation took 26.2ms | |
| elaboration: tactic compilation took 7.01ms | |
| elaboration: tactic compilation took 4.75ms | |
| elaboration: tactic execution took 1ms | |
| num. allocated objects: 32 | |
| num. allocated closures: 44 | |
| 1ms 100.0% interaction_monad_orelse | |
| 1ms 100.0% scope_trace | |
| 1ms 100.0% tactic.istep._lambda_1 | |
| 1ms 100.0% tactic.focus1 | |
| 1ms 100.0% tactic.subst_core | |
| 1ms 100.0% tactic.rintro._lambda_3 | |
| 1ms 100.0% tactic.istep | |
| 1ms 100.0% tactic.seq | |
| 1ms 100.0% _interaction._lambda_2 | |
| 1ms 100.0% tactic.step | |
| 1ms 100.0% tactic.rintro | |
| 1ms 100.0% tactic.rcases.continue | |
| 1ms 100.0% tactic.interactive.rintro | |
| elaboration: tactic execution took 848ms | |
| num. allocated objects: 3028 | |
| num. allocated closures: 2916 | |
| 848ms 100.0% tactic.solve1 | |
| 848ms 100.0% tactic.istep._lambda_1 | |
| 848ms 100.0% _interaction._lambda_2 | |
| 848ms 100.0% scope_trace | |
| 848ms 100.0% tactic.istep | |
| 848ms 100.0% tactic.step | |
| 543ms 64.0% tactic.cc_core | |
| 542ms 63.9% cc_state.mk_using_hs_core | |
| 205ms 24.2% tactic.interactive.propagate_tags | |
| 127ms 15.0% tactic.to_expr | |
| 106ms 12.5% interaction_monad_orelse | |
| 105ms 12.4% tactic.interactive.simp_core | |
| 103ms 12.1% interaction_monad.monad._lambda_9 | |
| 100ms 11.8% tactic.interactive.simp_core_aux | |
| 100ms 11.8% tactic.interactive.simp_core_aux._lambda_5 | |
| 100ms 11.8% tactic.simp_target | |
| 100ms 11.8% rw_core | |
| 97ms 11.4% tactic.simplify | |
| 97ms 11.4% interactive.loc.apply | |
| 97ms 11.4% interaction_monad.orelse' | |
| 94ms 11.1% _private.3132620493.rw_goal._lambda_4 | |
| 94ms 11.1% _private.3132620493.rw_goal._lambda_2 | |
| 51ms 6.0% tactic.rewrite_target | |
| 48ms 5.7% tactic.rewrite | |
| 48ms 5.7% tactic.rewrite_core | |
| 43ms 5.1% tactic.interactive.to_expr' | |
| 42ms 5.0% tactic.interactive.have._lambda_1 | |
| 33ms 3.9% tactic.interactive.exact | |
| 12ms 1.4% tactic.refine | |
| 9ms 1.1% tactic.replace_target | |
| 7ms 0.8% tactic.rintro | |
| 7ms 0.8% tactic.interactive.rintro | |
| 6ms 0.7% tactic.rcases_core | |
| 6ms 0.7% relation_tactic | |
| 6ms 0.7% tactic.rcases.continue | |
| 6ms 0.7% tactic.rintro._lambda_3 | |
| 6ms 0.7% tactic.rcases_core._main._lambda_5 | |
| 6ms 0.7% tactic.focus1 | |
| 6ms 0.7% _private.878893113.relation_tactic._lambda_1 | |
| 5ms 0.6% simp_lemmas.add_pexpr | |
| 5ms 0.6% _private.4232751329.simp_lemmas.resolve_and_add._lambda_2 | |
| 5ms 0.6% tactic.apply_core | |
| 5ms 0.6% tactic.mk_simp_set_core | |
| 5ms 0.6% simp_lemmas.resolve_and_add | |
| 5ms 0.6% simp_lemmas.append_pexprs | |
| 5ms 0.6% tactic.mk_simp_set | |
| 4ms 0.5% tactic.cases_core | |
| 4ms 0.5% tactic.rcases_core._main._lambda_2 | |
| 4ms 0.5% tactic.exact | |
| 4ms 0.5% is_valid_simp_lemma_cnst | |
| 4ms 0.5% tactic.rcases_core._main._lambda_3 | |
| 4ms 0.5% char.of_nat | |
| 3ms 0.4% tactic.rewrite_hyp | |
| 3ms 0.4% tactic.mk_app | |
| 3ms 0.4% _private.1542453965.rw_hyp._main._lambda_2 | |
| 3ms 0.4% rw_hyp | |
| 3ms 0.4% tactic.mk_id_eq | |
| 3ms 0.4% tactic.rcases.continue._main._lambda_2 | |
| 3ms 0.4% _private.1542453965.rw_hyp._main._lambda_3 | |
| 3ms 0.4% tactic.assert | |
| 2ms 0.2% tactic.assert_core | |
| 2ms 0.2% tactic.mk_eq_mpr | |
| 2ms 0.2% and.decidable | |
| 2ms 0.2% tactic.reflexivity | |
| 1ms 0.1% assume_core | |
| 1ms 0.1% tactic.mk_const | |
| 1ms 0.1% tactic.intro_core | |
| 1ms 0.1% cc_state.proof_for_false | |
| 1ms 0.1% tactic.try_core | |
| 1ms 0.1% declaration.univ_params | |
| 1ms 0.1% tactic.intro | |
| 1ms 0.1% tactic.interactive.assume | |
| 1ms 0.1% tactic.try | |
| 1ms 0.1% simp_lemmas.add_simp | |
| 1ms 0.1% tactic.rintro._lambda_2 | |
| 1ms 0.1% tactic.subst_core | |
| elaboration: tactic execution took 49ms | |
| num. allocated objects: 49 | |
| num. allocated closures: 58 | |
| 49ms 100.0% cc_state.mk_using_hs_core | |
| 49ms 100.0% tactic.step | |
| 49ms 100.0% scope_trace | |
| 49ms 100.0% tactic.istep._lambda_1 | |
| 49ms 100.0% tactic.cc_core | |
| 49ms 100.0% all_goals_core | |
| 49ms 100.0% tactic.istep | |
| 49ms 100.0% tactic.seq | |
| 49ms 100.0% tactic.all_goals | |
| 49ms 100.0% interaction_monad.monad._lambda_9 | |
| 49ms 100.0% _private.3864167971.all_goals_core._main._lambda_2 | |
| elaboration of prod_sum took 1.29s | |
| elaboration: tactic execution took 95ms | |
| num. allocated objects: 1843 | |
| num. allocated closures: 1668 | |
| 95ms 100.0% tactic.step | |
| 95ms 100.0% tactic.istep | |
| 95ms 100.0% scope_trace | |
| 95ms 100.0% _interaction._lambda_2 | |
| 95ms 100.0% tactic.istep._lambda_1 | |
| 93ms 97.9% tactic.solve1 | |
| 64ms 67.4% tactic.to_expr | |
| 57ms 60.0% tactic.interactive.exact | |
| 31ms 32.6% interaction_monad.monad._lambda_9 | |
| 30ms 31.6% tactic.interactive.propagate_tags | |
| 29ms 30.5% interaction_monad.orelse' | |
| 29ms 30.5% rw_core | |
| 29ms 30.5% interactive.loc.apply | |
| 28ms 29.5% _private.3132620493.rw_goal._lambda_2 | |
| 28ms 29.5% _private.3132620493.rw_goal._lambda_4 | |
| 24ms 25.3% tactic.rewrite_target | |
| 15ms 15.8% tactic.rewrite | |
| 13ms 13.7% tactic.rewrite_core | |
| 10ms 10.5% tactic.replace_target | |
| 7ms 7.4% tactic.interactive.rwa | |
| 7ms 7.4% tactic.mk_eq_mpr | |
| 4ms 4.2% tactic.interactive.to_expr' | |
| 3ms 3.2% tactic.interactive.have._lambda_1 | |
| 3ms 3.2% tactic.try_core | |
| 3ms 3.2% interaction_monad_orelse | |
| 3ms 3.2% tactic.assumption._lambda_1 | |
| 3ms 3.2% tactic.find_same_type | |
| 3ms 3.2% tactic.try | |
| 2ms 2.1% tactic.interactive.by_cases | |
| 2ms 2.1% tactic.by_cases | |
| 2ms 2.1% tactic.interactive.concat_tags._lambda_5 | |
| 2ms 2.1% tactic.interactive.by_cases._lambda_2 | |
| 2ms 2.1% tactic.unify | |
| 2ms 2.1% tactic.find_same_type._main._lambda_1 | |
| 2ms 2.1% tactic.exact | |
| 2ms 2.1% tactic.has_opt_auto_param._lambda_2 | |
| 1ms 1.1% tactic.intro_lst | |
| 1ms 1.1% tactic.intro | |
| 1ms 1.1% rw_hyp | |
| 1ms 1.1% _private.1542453965.rw_hyp._main._lambda_2 | |
| 1ms 1.1% expr.const | |
| 1ms 1.1% char.of_nat | |
| 1ms 1.1% tactic.rewrite_hyp | |
| 1ms 1.1% tactic.mk_mapp | |
| 1ms 1.1% _private.1542453965.rw_hyp._main._lambda_3 | |
| 1ms 1.1% expr.is_napp_of | |
| 1ms 1.1% tactic.interactive.intros._lambda_2 | |
| 1ms 1.1% tactic.assert_core | |
| 1ms 1.1% tactic.interactive.intros | |
| 1ms 1.1% tactic.intro_core | |
| 1ms 1.1% expr.get_app_fn | |
| 1ms 1.1% tactic.assert | |
| 1ms 1.1% expr.is_app_of | |
| elaboration of to_finset_sum_count_eq took 299ms | |
| cumulative profiling times: | |
| compilation 1.61ms | |
| decl post-processing 4.23s | |
| elaboration 5.67s | |
| elaboration: tactic compilation 469ms | |
| elaboration: tactic execution 2.71s | |
| parsing 968ms | |
| type checking 15.2ms |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment