-
-
Save kckennylau/ed020e947bc2501f54d7f944b6bac2b9 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
| git ls-files *.lean | xargs -I % sh -c '>&2 echo %; /c/{redacted}/.elan/toolchains/leanprover-community-lean-3.11.0/bin/lean --profile % >/dev/null;' > profile.txt 2>&1 | |
| archive/cubing_a_cube.lean | |
| cumulative profiling times: | |
| compilation 27.4ms | |
| decl post-processing 304ms | |
| elaboration 63.7s | |
| elaboration: tactic compilation 1.62s | |
| elaboration: tactic execution 54.5s | |
| parsing 8.56s | |
| type checking 204ms | |
| archive/examples/prop_encodable.lean | |
| cumulative profiling times: | |
| compilation 8.08ms | |
| decl post-processing 47.2ms | |
| elaboration 2.76s | |
| elaboration: tactic compilation 109ms | |
| elaboration: tactic execution 3.58s | |
| parsing 84ms | |
| type checking 1.06ms | |
| archive/imo1988_q6.lean | |
| cumulative profiling times: | |
| compilation 0.0069ms | |
| decl post-processing 0.0109ms | |
| elaboration 17.3s | |
| elaboration: tactic compilation 1.37s | |
| elaboration: tactic execution 38.7s | |
| parsing 2.49s | |
| type checking 0.94ms | |
| archive/sensitivity.lean | |
| cumulative profiling times: | |
| compilation 24.8ms | |
| decl post-processing 418ms | |
| elaboration 105s | |
| elaboration: tactic compilation 1.26s | |
| elaboration: tactic execution 103s | |
| parsing 3.49s | |
| type checking 168ms | |
| docs/tutorial/Zmod37.lean | |
| cumulative profiling times: | |
| compilation 13.9ms | |
| decl post-processing 25.1ms | |
| elaboration 6.03s | |
| elaboration: tactic compilation 254ms | |
| elaboration: tactic execution 4.57s | |
| parsing 410ms | |
| type checking 5.02ms | |
| docs/tutorial/category_theory/Ab.lean | |
| cumulative profiling times: | |
| parsing 0.397ms | |
| docs/tutorial/category_theory/calculating_colimits_in_Top.lean | |
| cumulative profiling times: | |
| compilation 14.5ms | |
| decl post-processing 49.9ms | |
| elaboration 1.4s | |
| elaboration: tactic compilation 25.1ms | |
| elaboration: tactic execution 120ms | |
| parsing 46ms | |
| type checking 27ms | |
| docs/tutorial/category_theory/intro.lean | |
| cumulative profiling times: | |
| parsing 3.76ms | |
| roadmap/todo.lean | |
| cumulative profiling times: | |
| compilation 4ms | |
| decl post-processing 0.0047ms | |
| elaboration 2.96ms | |
| parsing 1.05ms | |
| type checking 0.204ms | |
| roadmap/topology/paracompact.lean | |
| cumulative profiling times: | |
| compilation 6.27ms | |
| decl post-processing 0.0172ms | |
| elaboration 243ms | |
| elaboration: tactic compilation 72.6ms | |
| elaboration: tactic execution 71ms | |
| parsing 91.1ms | |
| type checking 0.837ms | |
| roadmap/topology/shrinking_lemma.lean | |
| cumulative profiling times: | |
| compilation 6.35ms | |
| decl post-processing 0.0125ms | |
| elaboration 4.08ms | |
| parsing 2.55ms | |
| type checking 0.787ms | |
| scripts/lean_version.lean | |
| cumulative profiling times: | |
| compilation 2.58ms | |
| decl post-processing 0.46ms | |
| elaboration 9.21ms | |
| parsing 11.8ms | |
| type checking 0.0154ms | |
| scripts/lint_mathlib.lean | |
| cumulative profiling times: | |
| compilation 64.5ms | |
| decl post-processing 0.0899ms | |
| elaboration 133ms | |
| parsing 3.05ms | |
| type checking 5.12ms | |
| src/algebra/archimedean.lean | |
| cumulative profiling times: | |
| compilation 15.7ms | |
| decl post-processing 35.1ms | |
| elaboration 10.3s | |
| elaboration: tactic compilation 478ms | |
| elaboration: tactic execution 7.98s | |
| parsing 1.21s | |
| type checking 53.3ms | |
| src/algebra/associated.lean | |
| cumulative profiling times: | |
| compilation 70.8ms | |
| decl post-processing 68.7ms | |
| elaboration 42.9s | |
| elaboration: tactic compilation 1.4s | |
| elaboration: tactic execution 33.4s | |
| parsing 2.95s | |
| type checking 89.1ms | |
| src/algebra/big_operators.lean | |
| cumulative profiling times: | |
| compilation 2.22ms | |
| decl post-processing 35.2s | |
| elaboration 103s | |
| elaboration: tactic compilation 2.64s | |
| elaboration: tactic execution 107s | |
| parsing 5.85s | |
| type checking 65.9ms | |
| src/algebra/category/CommRing/adjunctions.lean | |
| cumulative profiling times: | |
| compilation 0.0173ms | |
| decl post-processing 65ms | |
| elaboration 6.97s | |
| elaboration: tactic compilation 34.4ms | |
| elaboration: tactic execution 6.14s | |
| parsing 35.2ms | |
| type checking 71.9ms | |
| src/algebra/category/CommRing/basic.lean | |
| cumulative profiling times: | |
| compilation 115ms | |
| decl post-processing 363ms | |
| elaboration 43.2s | |
| elaboration: tactic compilation 200ms | |
| elaboration: tactic execution 43.4s | |
| parsing 74.3ms | |
| type checking 210ms | |
| src/algebra/category/CommRing/colimits.lean | |
| cumulative profiling times: | |
| compilation 76.7ms | |
| decl post-processing 332ms | |
| elaboration 34.6s | |
| elaboration: tactic compilation 578ms | |
| elaboration: tactic execution 23s | |
| parsing 1.51s | |
| type checking 249ms | |
| src/algebra/category/CommRing/default.lean | |
| src/algebra/category/CommRing/limits.lean | |
| cumulative profiling times: | |
| compilation 166ms | |
| decl post-processing 316ms | |
| elaboration 10.4s | |
| elaboration: tactic compilation 219ms | |
| elaboration: tactic execution 6.95s | |
| parsing 454ms | |
| type checking 257ms | |
| src/algebra/category/Group/Z_Module_equivalence.lean | |
| cumulative profiling times: | |
| compilation 45.9ms | |
| decl post-processing 19.6ms | |
| elaboration 5.99s | |
| elaboration: tactic compilation 9.74ms | |
| elaboration: tactic execution 5.5s | |
| parsing 26.6ms | |
| type checking 16.9ms | |
| src/algebra/category/Group/adjunctions.lean | |
| cumulative profiling times: | |
| compilation 34.8ms | |
| decl post-processing 30.1ms | |
| elaboration 13.5s | |
| elaboration: tactic compilation 62.4ms | |
| elaboration: tactic execution 12.2s | |
| parsing 78ms | |
| type checking 26ms | |
| src/algebra/category/Group/basic.lean | |
| cumulative profiling times: | |
| compilation 85.5ms | |
| decl post-processing 49.6s | |
| elaboration 50.1s | |
| elaboration: tactic compilation 233ms | |
| elaboration: tactic execution 51.3s | |
| parsing 457ms | |
| type checking 223ms | |
| src/algebra/category/Group/biproducts.lean | |
| cumulative profiling times: | |
| compilation 402ms | |
| decl post-processing 323ms | |
| elaboration 52.3s | |
| elaboration: tactic compilation 281ms | |
| elaboration: tactic execution 44.7s | |
| parsing 1.1s | |
| type checking 216ms | |
| src/algebra/category/Group/colimits.lean | |
| cumulative profiling times: | |
| compilation 78.3ms | |
| decl post-processing 207ms | |
| elaboration 24.5s | |
| elaboration: tactic compilation 339ms | |
| elaboration: tactic execution 17.2s | |
| parsing 930ms | |
| type checking 141ms | |
| src/algebra/category/Group/default.lean | |
| src/algebra/category/Group/images.lean | |
| cumulative profiling times: | |
| compilation 32ms | |
| decl post-processing 53.1ms | |
| elaboration 6.67s | |
| elaboration: tactic compilation 73.6ms | |
| elaboration: tactic execution 5.38s | |
| parsing 314ms | |
| type checking 46.1ms | |
| src/algebra/category/Group/limits.lean | |
| cumulative profiling times: | |
| compilation 179ms | |
| decl post-processing 174ms | |
| elaboration 10.7s | |
| elaboration: tactic compilation 174ms | |
| elaboration: tactic execution 8.14s | |
| parsing 287ms | |
| type checking 151ms | |
| src/algebra/category/Group/zero.lean | |
| cumulative profiling times: | |
| compilation 26.4ms | |
| decl post-processing 11.3ms | |
| elaboration 5.52s | |
| elaboration: tactic compilation 33.3ms | |
| elaboration: tactic execution 4.85s | |
| parsing 61.8ms | |
| type checking 7.86ms | |
| src/algebra/category/Module/basic.lean | |
| cumulative profiling times: | |
| compilation 177ms | |
| decl post-processing 325ms | |
| elaboration 37.7s | |
| elaboration: tactic compilation 215ms | |
| elaboration: tactic execution 33s | |
| parsing 310ms | |
| type checking 168ms | |
| src/algebra/category/Module/monoidal.lean | |
| cumulative profiling times: | |
| compilation 61.8ms | |
| decl post-processing 87.2ms | |
| elaboration 67.4s | |
| elaboration: tactic compilation 148ms | |
| elaboration: tactic execution 62.9s | |
| parsing 311ms | |
| type checking 90.9ms | |
| src/algebra/category/Mon/basic.lean | |
| cumulative profiling times: | |
| compilation 62.2ms | |
| decl post-processing 41.7s | |
| elaboration 33.5s | |
| elaboration: tactic compilation 160ms | |
| elaboration: tactic execution 33.1s | |
| parsing 81.7ms | |
| type checking 45.7ms | |
| src/algebra/category/Mon/colimits.lean | |
| cumulative profiling times: | |
| compilation 41.7ms | |
| decl post-processing 109ms | |
| elaboration 21.4s | |
| elaboration: tactic compilation 281ms | |
| elaboration: tactic execution 16.2s | |
| parsing 781ms | |
| type checking 46.2ms | |
| src/algebra/category/Mon/default.lean | |
| src/algebra/char_p.lean | |
| cumulative profiling times: | |
| compilation 6.58ms | |
| decl post-processing 41.2ms | |
| elaboration 12.4s | |
| elaboration: tactic compilation 563ms | |
| elaboration: tactic execution 10.1s | |
| parsing 943ms | |
| type checking 62.3ms | |
| src/algebra/char_zero.lean | |
| cumulative profiling times: | |
| compilation 0.413ms | |
| decl post-processing 99.3ms | |
| elaboration 1.16s | |
| elaboration: tactic compilation 170ms | |
| elaboration: tactic execution 438ms | |
| parsing 286ms | |
| type checking 14.2ms | |
| src/algebra/classical_lie_algebras.lean | |
| cumulative profiling times: | |
| compilation 35.6ms | |
| decl post-processing 45.3ms | |
| elaboration 16.2s | |
| elaboration: tactic compilation 139ms | |
| elaboration: tactic execution 18.1s | |
| parsing 463ms | |
| type checking 50ms | |
| src/algebra/commute.lean | |
| cumulative profiling times: | |
| compilation 13.1ms | |
| decl post-processing 102ms | |
| elaboration 3.39s | |
| elaboration: tactic compilation 209ms | |
| elaboration: tactic execution 739ms | |
| parsing 323ms | |
| type checking 48.4ms | |
| src/algebra/continued_fractions/basic.lean | |
| cumulative profiling times: | |
| compilation 56.6ms | |
| decl post-processing 133ms | |
| elaboration 1.37s | |
| elaboration: tactic compilation 88ms | |
| elaboration: tactic execution 721ms | |
| parsing 89.9ms | |
| type checking 7.96ms | |
| src/algebra/continued_fractions/continuants_recurrence.lean | |
| cumulative profiling times: | |
| compilation 0.0153ms | |
| decl post-processing 0.0245ms | |
| elaboration 2.47s | |
| elaboration: tactic compilation 95.6ms | |
| elaboration: tactic execution 2.07s | |
| parsing 178ms | |
| type checking 3.48ms | |
| src/algebra/continued_fractions/convergents_equiv.lean | |
| cumulative profiling times: | |
| compilation 11.1ms | |
| decl post-processing 5.98ms | |
| elaboration 18.2s | |
| elaboration: tactic compilation 941ms | |
| elaboration: tactic execution 16.3s | |
| parsing 4.57s | |
| type checking 5.46ms | |
| src/algebra/continued_fractions/default.lean | |
| src/algebra/continued_fractions/terminated_stable.lean | |
| cumulative profiling times: | |
| compilation 0.0309ms | |
| decl post-processing 0.0452ms | |
| elaboration 1.93s | |
| elaboration: tactic compilation 223ms | |
| elaboration: tactic execution 1.16s | |
| parsing 1.06s | |
| type checking 1.99ms | |
| src/algebra/continued_fractions/translations.lean | |
| cumulative profiling times: | |
| compilation 0.0748ms | |
| decl post-processing 3.28ms | |
| elaboration 7.11s | |
| elaboration: tactic compilation 207ms | |
| elaboration: tactic execution 6.13s | |
| parsing 397ms | |
| type checking 7.09ms | |
| src/algebra/default.lean | |
| src/algebra/direct_limit.lean | |
| cumulative profiling times: | |
| compilation 588ms | |
| decl post-processing 5.28s | |
| elaboration 45s | |
| elaboration: tactic compilation 1.03s | |
| elaboration: tactic execution 34s | |
| parsing 2.08s | |
| type checking 7.5s | |
| src/algebra/direct_sum.lean | |
| cumulative profiling times: | |
| compilation 57.7ms | |
| decl post-processing 217ms | |
| elaboration 8.91s | |
| elaboration: tactic compilation 250ms | |
| elaboration: tactic execution 4.54s | |
| parsing 798ms | |
| type checking 170ms | |
| src/algebra/euclidean_domain.lean | |
| cumulative profiling times: | |
| compilation 49.4ms | |
| decl post-processing 69ms | |
| elaboration 13.1s | |
| elaboration: tactic compilation 1.07s | |
| elaboration: tactic execution 3.34s | |
| parsing 2.27s | |
| type checking 36ms | |
| src/algebra/field.lean | |
| cumulative profiling times: | |
| compilation 45.6ms | |
| decl post-processing 34.3ms | |
| elaboration 4.13s | |
| elaboration: tactic compilation 359ms | |
| elaboration: tactic execution 2.54s | |
| parsing 566ms | |
| type checking 40.7ms | |
| src/algebra/field_power.lean | |
| cumulative profiling times: | |
| compilation 0.0573ms | |
| decl post-processing 82.2ms | |
| elaboration 12.8s | |
| elaboration: tactic compilation 487ms | |
| elaboration: tactic execution 11s | |
| parsing 1.47s | |
| type checking 14.2ms | |
| src/algebra/floor.lean | |
| cumulative profiling times: | |
| compilation 45.3ms | |
| decl post-processing 20.7ms | |
| elaboration 28.4s | |
| elaboration: tactic compilation 1.01s | |
| elaboration: tactic execution 26.9s | |
| parsing 2.11s | |
| type checking 66.8ms | |
| src/algebra/free.lean | |
| cumulative profiling times: | |
| compilation 147ms | |
| decl post-processing 715ms | |
| elaboration 7.56s | |
| elaboration: tactic compilation 691ms | |
| elaboration: tactic execution 3.82s | |
| parsing 1.14s | |
| type checking 574ms | |
| src/algebra/free_monoid.lean | |
| cumulative profiling times: | |
| compilation 26ms | |
| decl post-processing 9.61s | |
| elaboration 2.65s | |
| elaboration: tactic compilation 152ms | |
| elaboration: tactic execution 1.93s | |
| parsing 208ms | |
| type checking 31ms | |
| src/algebra/gcd_domain.lean | |
| cumulative profiling times: | |
| compilation 96.1ms | |
| decl post-processing 145ms | |
| elaboration 54.4s | |
| elaboration: tactic compilation 1.68s | |
| elaboration: tactic execution 43.8s | |
| parsing 2.97s | |
| type checking 143ms | |
| src/algebra/geom_sum.lean | |
| cumulative profiling times: | |
| compilation 16.4ms | |
| decl post-processing 7.98ms | |
| elaboration 14.1s | |
| elaboration: tactic compilation 646ms | |
| elaboration: tactic execution 14.5s | |
| parsing 1.58s | |
| type checking 12.5ms | |
| src/algebra/group/anti_hom.lean | |
| cumulative profiling times: | |
| compilation 0.0118ms | |
| decl post-processing 0.0187ms | |
| elaboration 109ms | |
| elaboration: tactic compilation 36.9ms | |
| elaboration: tactic execution 5ms | |
| parsing 45.6ms | |
| type checking 0.904ms | |
| src/algebra/group/basic.lean | |
| cumulative profiling times: | |
| compilation 15.5ms | |
| decl post-processing 3.95s | |
| elaboration 3.89s | |
| elaboration: tactic compilation 700ms | |
| elaboration: tactic execution 1.64s | |
| parsing 1.05s | |
| type checking 23.6ms | |
| src/algebra/group/conj.lean | |
| cumulative profiling times: | |
| compilation 0.24ms | |
| decl post-processing 6.28ms | |
| elaboration 1.28s | |
| elaboration: tactic compilation 189ms | |
| elaboration: tactic execution 521ms | |
| parsing 268ms | |
| type checking 1.95ms | |
| src/algebra/group/default.lean | |
| src/algebra/group/hom.lean | |
| cumulative profiling times: | |
| compilation 75.4ms | |
| decl post-processing 5.95s | |
| elaboration 3.22s | |
| elaboration: tactic compilation 403ms | |
| elaboration: tactic execution 1.32s | |
| parsing 626ms | |
| type checking 74.9ms | |
| src/algebra/group/is_unit.lean | |
| cumulative profiling times: | |
| compilation 0.269ms | |
| decl post-processing 3.65s | |
| elaboration 987ms | |
| elaboration: tactic compilation 128ms | |
| elaboration: tactic execution 448ms | |
| parsing 145ms | |
| type checking 10.4ms | |
| src/algebra/group/prod.lean | |
| cumulative profiling times: | |
| compilation 83.8ms | |
| decl post-processing 12.7s | |
| elaboration 4.85s | |
| elaboration: tactic compilation 84.9ms | |
| elaboration: tactic execution 2.25s | |
| parsing 141ms | |
| type checking 80.8ms | |
| src/algebra/group/to_additive.lean | |
| cumulative profiling times: | |
| compilation 132ms | |
| decl post-processing 1.09ms | |
| elaboration 633ms | |
| elaboration: tactic compilation 0.491ms | |
| elaboration: tactic execution 0ms | |
| parsing 9.93ms | |
| type checking 8.92ms | |
| src/algebra/group/type_tags.lean | |
| cumulative profiling times: | |
| compilation 67.7ms | |
| decl post-processing 73.1ms | |
| elaboration 406ms | |
| parsing 7.16ms | |
| type checking 39.3ms | |
| src/algebra/group/units.lean | |
| cumulative profiling times: | |
| compilation 31.4ms | |
| decl post-processing 2.3s | |
| elaboration 1.18s | |
| elaboration: tactic compilation 326ms | |
| elaboration: tactic execution 69ms | |
| parsing 459ms | |
| type checking 33.7ms | |
| src/algebra/group/units_hom.lean | |
| cumulative profiling times: | |
| compilation 19.7ms | |
| decl post-processing 1.99s | |
| elaboration 610ms | |
| elaboration: tactic compilation 104ms | |
| elaboration: tactic execution 49ms | |
| parsing 144ms | |
| type checking 30.1ms | |
| src/algebra/group/with_one.lean | |
| cumulative profiling times: | |
| compilation 51.9ms | |
| decl post-processing 3.08s | |
| elaboration 4.89s | |
| elaboration: tactic compilation 249ms | |
| elaboration: tactic execution 3.16s | |
| parsing 592ms | |
| type checking 25.5ms | |
| src/algebra/group_power.lean | |
| cumulative profiling times: | |
| compilation 24ms | |
| decl post-processing 253ms | |
| elaboration 25.2s | |
| elaboration: tactic compilation 1.76s | |
| elaboration: tactic execution 15.5s | |
| parsing 3.42s | |
| type checking 80.8ms | |
| src/algebra/group_ring_action.lean | |
| cumulative profiling times: | |
| compilation 32.5ms | |
| decl post-processing 55ms | |
| elaboration 2.23s | |
| elaboration: tactic compilation 35.2ms | |
| elaboration: tactic execution 264ms | |
| parsing 101ms | |
| type checking 27.4ms | |
| src/algebra/group_with_zero.lean | |
| cumulative profiling times: | |
| compilation 11.8ms | |
| decl post-processing 28.3ms | |
| elaboration 14.6s | |
| elaboration: tactic compilation 1.55s | |
| elaboration: tactic execution 9.26s | |
| parsing 2.33s | |
| type checking 35.7ms | |
| src/algebra/group_with_zero_power.lean | |
| cumulative profiling times: | |
| compilation 2.12ms | |
| decl post-processing 10.4ms | |
| elaboration 3.73s | |
| elaboration: tactic compilation 480ms | |
| elaboration: tactic execution 1.45s | |
| parsing 743ms | |
| type checking 12.5ms | |
| src/algebra/homology/chain_complex.lean | |
| cumulative profiling times: | |
| compilation 18.1ms | |
| decl post-processing 18ms | |
| elaboration 143ms | |
| elaboration: tactic compilation 15.1ms | |
| elaboration: tactic execution 2.89s | |
| parsing 24.8ms | |
| type checking 59.1ms | |
| src/algebra/homology/homology.lean | |
| cumulative profiling times: | |
| compilation 193ms | |
| decl post-processing 2.31s | |
| elaboration 68.3s | |
| elaboration: tactic compilation 155ms | |
| elaboration: tactic execution 64.4s | |
| parsing 333ms | |
| type checking 119ms | |
| src/algebra/invertible.lean | |
| cumulative profiling times: | |
| compilation 56ms | |
| decl post-processing 63ms | |
| elaboration 13.5s | |
| elaboration: tactic compilation 281ms | |
| elaboration: tactic execution 11.1s | |
| parsing 350ms | |
| type checking 22.1ms | |
| src/algebra/lie_algebra.lean | |
| cumulative profiling times: | |
| compilation 371ms | |
| decl post-processing 553ms | |
| elaboration 78.9s | |
| elaboration: tactic compilation 1.04s | |
| elaboration: tactic execution 72.5s | |
| parsing 2.17s | |
| type checking 421ms | |
| src/algebra/midpoint.lean | |
| cumulative profiling times: | |
| compilation 10.2ms | |
| decl post-processing 15.7ms | |
| elaboration 2.76s | |
| elaboration: tactic compilation 223ms | |
| elaboration: tactic execution 660ms | |
| parsing 333ms | |
| type checking 29.9ms | |
| src/algebra/module.lean | |
| cumulative profiling times: | |
| compilation 161ms | |
| decl post-processing 716ms | |
| elaboration 55.2s | |
| elaboration: tactic compilation 877ms | |
| elaboration: tactic execution 61.6s | |
| parsing 1.85s | |
| type checking 232ms | |
| src/algebra/opposites.lean | |
| cumulative profiling times: | |
| compilation 102ms | |
| decl post-processing 87.7ms | |
| elaboration 299ms | |
| parsing 8.49ms | |
| type checking 57.4ms | |
| src/algebra/order.lean | |
| cumulative profiling times: | |
| compilation 8.18ms | |
| decl post-processing 9.7ms | |
| elaboration 2.03s | |
| elaboration: tactic compilation 282ms | |
| elaboration: tactic execution 953ms | |
| parsing 186ms | |
| type checking 16.4ms | |
| src/algebra/order_functions.lean | |
| cumulative profiling times: | |
| compilation 0.513ms | |
| decl post-processing 8.2ms | |
| elaboration 13.1s | |
| elaboration: tactic compilation 679ms | |
| elaboration: tactic execution 9.75s | |
| parsing 1.14s | |
| type checking 31.9ms | |
| src/algebra/ordered_field.lean | |
| cumulative profiling times: | |
| compilation 0.816ms | |
| decl post-processing 65.4ms | |
| elaboration 5.12s | |
| elaboration: tactic compilation 408ms | |
| elaboration: tactic execution 3.99s | |
| parsing 693ms | |
| type checking 90ms | |
| src/algebra/ordered_group.lean | |
| cumulative profiling times: | |
| compilation 193ms | |
| decl post-processing 223ms | |
| elaboration 18.8s | |
| elaboration: tactic compilation 1.36s | |
| elaboration: tactic execution 10.4s | |
| parsing 2.53s | |
| type checking 211ms | |
| src/algebra/ordered_ring.lean | |
| cumulative profiling times: | |
| compilation 200ms | |
| decl post-processing 200ms | |
| elaboration 20.8s | |
| elaboration: tactic compilation 1.04s | |
| elaboration: tactic execution 14.7s | |
| parsing 2.14s | |
| type checking 198ms | |
| src/algebra/pi_instances.lean | |
| cumulative profiling times: | |
| compilation 265ms | |
| decl post-processing 26.8s | |
| elaboration 37.6s | |
| elaboration: tactic compilation 575ms | |
| elaboration: tactic execution 33.4s | |
| parsing 816ms | |
| type checking 296ms | |
| src/algebra/pointwise.lean | |
| cumulative profiling times: | |
| compilation 50.6ms | |
| decl post-processing 38.4s | |
| elaboration 18s | |
| elaboration: tactic compilation 923ms | |
| elaboration: tactic execution 13.8s | |
| parsing 1.01s | |
| type checking 22ms | |
| src/algebra/punit_instances.lean | |
| cumulative profiling times: | |
| compilation 44ms | |
| decl post-processing 5.24s | |
| elaboration 793ms | |
| elaboration: tactic compilation 57.4ms | |
| elaboration: tactic execution 48ms | |
| parsing 28.6ms | |
| type checking 47.6ms | |
| src/algebra/quadratic_discriminant.lean | |
| cumulative profiling times: | |
| compilation 12.5ms | |
| decl post-processing 2.73ms | |
| elaboration 19.4s | |
| elaboration: tactic compilation 509ms | |
| elaboration: tactic execution 31.8s | |
| parsing 2.14s | |
| type checking 6.26ms | |
| src/algebra/ring.lean | |
| cumulative profiling times: | |
| compilation 126ms | |
| decl post-processing 807ms | |
| elaboration 20.9s | |
| elaboration: tactic compilation 1.71s | |
| elaboration: tactic execution 12.5s | |
| parsing 2.77s | |
| type checking 175ms | |
| src/algebra/semiconj.lean | |
| cumulative profiling times: | |
| compilation 0.274ms | |
| decl post-processing 36.1ms | |
| elaboration 2.26s | |
| elaboration: tactic compilation 331ms | |
| elaboration: tactic execution 763ms | |
| parsing 505ms | |
| type checking 12.8ms | |
| src/algebraic_geometry/presheafed_space.lean | |
| cumulative profiling times: | |
| compilation 131ms | |
| decl post-processing 167ms | |
| elaboration 26.7s | |
| elaboration: tactic compilation 221ms | |
| elaboration: tactic execution 22.7s | |
| parsing 840ms | |
| type checking 228ms | |
| src/algebraic_geometry/prime_spectrum.lean | |
| cumulative profiling times: | |
| compilation 12.7ms | |
| decl post-processing 81.8ms | |
| elaboration 36.5s | |
| elaboration: tactic compilation 660ms | |
| elaboration: tactic execution 31s | |
| parsing 1.7s | |
| type checking 57.7ms | |
| src/algebraic_geometry/stalks.lean | |
| cumulative profiling times: | |
| compilation 18.9ms | |
| decl post-processing 32.2ms | |
| elaboration 21.2s | |
| elaboration: tactic compilation 62.6ms | |
| elaboration: tactic execution 20s | |
| parsing 275ms | |
| type checking 43.8ms | |
| src/analysis/ODE/gronwall.lean | |
| cumulative profiling times: | |
| compilation 0.0634ms | |
| decl post-processing 4.79ms | |
| elaboration 3.63s | |
| elaboration: tactic compilation 338ms | |
| elaboration: tactic execution 2.16s | |
| parsing 1.46s | |
| type checking 15.3ms | |
| src/analysis/analytic/basic.lean | |
| cumulative profiling times: | |
| compilation 65.9ms | |
| decl post-processing 110ms | |
| elaboration 211s | |
| elaboration: tactic compilation 2.16s | |
| elaboration: tactic execution 280s | |
| parsing 8.74s | |
| type checking 210ms | |
| src/analysis/analytic/composition.lean | |
| cumulative profiling times: | |
| compilation 86.6ms | |
| decl post-processing 287ms | |
| elaboration 194s | |
| elaboration: tactic compilation 2.69s | |
| elaboration: tactic execution 201s | |
| parsing 9.74s | |
| type checking 239ms | |
| src/analysis/asymptotics.lean | |
| cumulative profiling times: | |
| compilation 1.8ms | |
| decl post-processing 25.6ms | |
| elaboration 32.5s | |
| elaboration: tactic compilation 876ms | |
| elaboration: tactic execution 26.4s | |
| parsing 2.35s | |
| type checking 121ms | |
| src/analysis/calculus/darboux.lean | |
| cumulative profiling times: | |
| compilation 0.0159ms | |
| decl post-processing 0.0315ms | |
| elaboration 8.08s | |
| elaboration: tactic compilation 182ms | |
| elaboration: tactic execution 7.22s | |
| parsing 704ms | |
| type checking 18.2ms | |
| src/analysis/calculus/deriv.lean | |
| cumulative profiling times: | |
| compilation 2.89ms | |
| decl post-processing 95.5ms | |
| elaboration 240s | |
| elaboration: tactic compilation 1.81s | |
| elaboration: tactic execution 228s | |
| parsing 4.77s | |
| type checking 1.08s | |
| src/analysis/calculus/extend_deriv.lean | |
| cumulative profiling times: | |
| compilation 0.0179ms | |
| decl post-processing 0.0245ms | |
| elaboration 50.9s | |
| elaboration: tactic compilation 352ms | |
| elaboration: tactic execution 48.7s | |
| parsing 2.72s | |
| type checking 46.5ms | |
| src/analysis/calculus/fderiv.lean | |
| cumulative profiling times: | |
| compilation 6.35ms | |
| decl post-processing 179ms | |
| elaboration 204s | |
| elaboration: tactic compilation 2.52s | |
| elaboration: tactic execution 199s | |
| parsing 7.48s | |
| type checking 2.6s | |
| src/analysis/calculus/inverse.lean | |
| cumulative profiling times: | |
| compilation 35.8ms | |
| decl post-processing 231ms | |
| elaboration 28.9s | |
| elaboration: tactic compilation 474ms | |
| elaboration: tactic execution 24s | |
| parsing 1.19s | |
| type checking 261ms | |
| src/analysis/calculus/iterated_deriv.lean | |
| cumulative profiling times: | |
| compilation 0.113ms | |
| decl post-processing 20.1ms | |
| elaboration 81.9s | |
| elaboration: tactic compilation 537ms | |
| elaboration: tactic execution 76.6s | |
| parsing 1.09s | |
| type checking 198ms | |
| src/analysis/calculus/local_extr.lean | |
| cumulative profiling times: | |
| compilation 0.604ms | |
| decl post-processing 6.37ms | |
| elaboration 40s | |
| elaboration: tactic compilation 562ms | |
| elaboration: tactic execution 35.3s | |
| parsing 1.4s | |
| type checking 216ms | |
| src/analysis/calculus/mean_value.lean | |
| cumulative profiling times: | |
| compilation 0.155ms | |
| decl post-processing 0.186ms | |
| elaboration 39.5s | |
| elaboration: tactic compilation 885ms | |
| elaboration: tactic execution 33.4s | |
| parsing 4.29s | |
| type checking 157ms | |
| src/analysis/calculus/specific_functions.lean | |
| cumulative profiling times: | |
| compilation 0.438ms | |
| decl post-processing 34ms | |
| elaboration 52s | |
| elaboration: tactic compilation 388ms | |
| elaboration: tactic execution 47.9s | |
| parsing 2.13s | |
| type checking 7.51ms | |
| src/analysis/calculus/tangent_cone.lean | |
| cumulative profiling times: | |
| compilation 1.69ms | |
| decl post-processing 11.8ms | |
| elaboration 48.2s | |
| elaboration: tactic compilation 898ms | |
| elaboration: tactic execution 43s | |
| parsing 3.01s | |
| type checking 50.7ms | |
| src/analysis/calculus/times_cont_diff.lean | |
| cumulative profiling times: | |
| compilation 62.6ms | |
| decl post-processing 820ms | |
| elaboration 205s | |
| elaboration: tactic compilation 3.19s | |
| elaboration: tactic execution 185s | |
| parsing 13.3s | |
| type checking 2.34s | |
| src/analysis/complex/basic.lean | |
| cumulative profiling times: | |
| compilation 0.967ms | |
| decl post-processing 552ms | |
| elaboration 117s | |
| elaboration: tactic compilation 497ms | |
| elaboration: tactic execution 130s | |
| parsing 1.02s | |
| type checking 1.5s | |
| src/analysis/complex/polynomial.lean | |
| cumulative profiling times: | |
| compilation 0.0065ms | |
| decl post-processing 0.0125ms | |
| elaboration 23.9s | |
| elaboration: tactic compilation 306ms | |
| elaboration: tactic execution 21.2s | |
| parsing 489ms | |
| type checking 0.931ms | |
| src/analysis/convex/basic.lean | |
| cumulative profiling times: | |
| compilation 2.66ms | |
| decl post-processing 30.2ms | |
| elaboration 89.3s | |
| elaboration: tactic compilation 2.19s | |
| elaboration: tactic execution 83.4s | |
| parsing 5.46s | |
| type checking 390ms | |
| src/analysis/convex/cone.lean | |
| cumulative profiling times: | |
| compilation 87.4ms | |
| decl post-processing 216ms | |
| elaboration 19.1s | |
| elaboration: tactic compilation 646ms | |
| elaboration: tactic execution 14.7s | |
| parsing 2.22s | |
| type checking 183ms | |
| src/analysis/convex/specific_functions.lean | |
| cumulative profiling times: | |
| compilation 0.0222ms | |
| decl post-processing 0.0261ms | |
| elaboration 19.2s | |
| elaboration: tactic compilation 223ms | |
| elaboration: tactic execution 17.5s | |
| parsing 605ms | |
| type checking 21.5ms | |
| src/analysis/convex/topology.lean | |
| cumulative profiling times: | |
| compilation 0.0559ms | |
| decl post-processing 3.15ms | |
| elaboration 10.6s | |
| elaboration: tactic compilation 260ms | |
| elaboration: tactic execution 7.88s | |
| parsing 593ms | |
| type checking 83ms | |
| src/analysis/mean_inequalities.lean | |
| cumulative profiling times: | |
| compilation 0.0383ms | |
| decl post-processing 0.0485ms | |
| elaboration 15.6s | |
| elaboration: tactic compilation 380ms | |
| elaboration: tactic execution 13.7s | |
| parsing 1.21s | |
| type checking 5.27ms | |
| src/analysis/normed_space/banach.lean | |
| cumulative profiling times: | |
| compilation 49.5ms | |
| decl post-processing 42ms | |
| elaboration 47.1s | |
| elaboration: tactic compilation 858ms | |
| elaboration: tactic execution 56s | |
| parsing 3.06s | |
| type checking 33.8ms | |
| src/analysis/normed_space/basic.lean | |
| cumulative profiling times: | |
| compilation 104ms | |
| decl post-processing 585ms | |
| elaboration 178s | |
| elaboration: tactic compilation 2.14s | |
| elaboration: tactic execution 165s | |
| parsing 5.08s | |
| type checking 386ms | |
| src/analysis/normed_space/bounded_linear_maps.lean | |
| cumulative profiling times: | |
| compilation 56ms | |
| decl post-processing 87.8ms | |
| elaboration 121s | |
| elaboration: tactic compilation 1.34s | |
| elaboration: tactic execution 125s | |
| parsing 2.58s | |
| type checking 361ms | |
| src/analysis/normed_space/finite_dimension.lean | |
| cumulative profiling times: | |
| compilation 52.7ms | |
| decl post-processing 121ms | |
| elaboration 37.9s | |
| elaboration: tactic compilation 441ms | |
| elaboration: tactic execution 34.6s | |
| parsing 2.79s | |
| type checking 234ms | |
| src/analysis/normed_space/hahn_banach.lean | |
| cumulative profiling times: | |
| compilation 0.0035ms | |
| decl post-processing 0.0094ms | |
| elaboration 22.1s | |
| elaboration: tactic compilation 48.2ms | |
| elaboration: tactic execution 21s | |
| parsing 134ms | |
| type checking 43ms | |
| src/analysis/normed_space/mazur_ulam.lean | |
| cumulative profiling times: | |
| compilation 0.0338ms | |
| decl post-processing 95.8ms | |
| elaboration 27.3s | |
| elaboration: tactic compilation 163ms | |
| elaboration: tactic execution 23.4s | |
| parsing 833ms | |
| type checking 161ms | |
| src/analysis/normed_space/multilinear.lean | |
| cumulative profiling times: | |
| compilation 150ms | |
| decl post-processing 4.51s | |
| elaboration 284s | |
| elaboration: tactic compilation 2.38s | |
| elaboration: tactic execution 275s | |
| parsing 7.37s | |
| type checking 5.73s | |
| src/analysis/normed_space/operator_norm.lean | |
| cumulative profiling times: | |
| compilation 102ms | |
| decl post-processing 969ms | |
| elaboration 88.9s | |
| elaboration: tactic compilation 1.7s | |
| elaboration: tactic execution 76.2s | |
| parsing 5.37s | |
| type checking 618ms | |
| src/analysis/normed_space/point_reflection.lean | |
| cumulative profiling times: | |
| compilation 5.36ms | |
| decl post-processing 9.46ms | |
| elaboration 8.4s | |
| elaboration: tactic compilation 91.3ms | |
| elaboration: tactic execution 7.57s | |
| parsing 152ms | |
| type checking 17.1ms | |
| src/analysis/normed_space/real_inner_product.lean | |
| cumulative profiling times: | |
| compilation 0.165ms | |
| decl post-processing 18.6ms | |
| elaboration 156s | |
| elaboration: tactic compilation 1.52s | |
| elaboration: tactic execution 184s | |
| parsing 6.89s | |
| type checking 57.8ms | |
| src/analysis/normed_space/riesz_lemma.lean | |
| cumulative profiling times: | |
| compilation 0.0036ms | |
| decl post-processing 0.0105ms | |
| elaboration 6.9s | |
| elaboration: tactic compilation 126ms | |
| elaboration: tactic execution 6.52s | |
| parsing 585ms | |
| type checking 16.3ms | |
| src/analysis/special_functions/exp_log.lean | |
| cumulative profiling times: | |
| compilation 0.227ms | |
| decl post-processing 11ms | |
| elaboration 74.1s | |
| elaboration: tactic compilation 1.27s | |
| elaboration: tactic execution 85.4s | |
| parsing 3.56s | |
| type checking 32.7ms | |
| src/analysis/special_functions/pow.lean | |
| cumulative profiling times: | |
| compilation 0.37ms | |
| decl post-processing 105ms | |
| elaboration 367s | |
| elaboration: tactic compilation 2.36s | |
| elaboration: tactic execution 253s | |
| parsing 6.28s | |
| type checking 23.4ms | |
| src/analysis/special_functions/trigonometric.lean | |
| cumulative profiling times: | |
| compilation 31.1ms | |
| decl post-processing 94.7ms | |
| elaboration 645s | |
| elaboration: tactic compilation 5.89s | |
| elaboration: tactic execution 566s | |
| parsing 11.7s | |
| type checking 148ms | |
| src/analysis/specific_limits.lean | |
| cumulative profiling times: | |
| compilation 0.216ms | |
| decl post-processing 4.85ms | |
| elaboration 51.7s | |
| elaboration: tactic compilation 1.18s | |
| elaboration: tactic execution 49.1s | |
| parsing 3.45s | |
| type checking 52.1ms | |
| src/category_theory/action.lean | |
| cumulative profiling times: | |
| compilation 27.8ms | |
| decl post-processing 68.8ms | |
| elaboration 1.32s | |
| elaboration: tactic compilation 19.7ms | |
| elaboration: tactic execution 716ms | |
| parsing 15.3ms | |
| type checking 36.3ms | |
| src/category_theory/adjunction/basic.lean | |
| cumulative profiling times: | |
| compilation 178ms | |
| decl post-processing 996ms | |
| elaboration 26s | |
| elaboration: tactic compilation 546ms | |
| elaboration: tactic execution 22.1s | |
| parsing 1.42s | |
| type checking 285ms | |
| src/category_theory/adjunction/default.lean | |
| src/category_theory/adjunction/fully_faithful.lean | |
| cumulative profiling times: | |
| compilation 75.2ms | |
| decl post-processing 99.9ms | |
| elaboration 14.3s | |
| elaboration: tactic compilation 93.4ms | |
| elaboration: tactic execution 12.9s | |
| parsing 289ms | |
| type checking 67.4ms | |
| src/category_theory/adjunction/limits.lean | |
| cumulative profiling times: | |
| compilation 482ms | |
| decl post-processing 933ms | |
| elaboration 96.8s | |
| elaboration: tactic compilation 174ms | |
| elaboration: tactic execution 90.7s | |
| parsing 314ms | |
| type checking 339ms | |
| src/category_theory/category/Cat.lean | |
| cumulative profiling times: | |
| compilation 12.4ms | |
| decl post-processing 17.5ms | |
| elaboration 190ms | |
| elaboration: tactic compilation 33.6ms | |
| elaboration: tactic execution 7ms | |
| parsing 23.7ms | |
| type checking 12.2ms | |
| src/category_theory/category/Groupoid.lean | |
| cumulative profiling times: | |
| compilation 27.8ms | |
| decl post-processing 57.1ms | |
| elaboration 10.6s | |
| elaboration: tactic compilation 40.4ms | |
| elaboration: tactic execution 9.71s | |
| parsing 22.6ms | |
| type checking 54ms | |
| src/category_theory/category/Kleisli.lean | |
| cumulative profiling times: | |
| compilation 22.6ms | |
| decl post-processing 16.7ms | |
| elaboration 352ms | |
| elaboration: tactic compilation 20.5ms | |
| elaboration: tactic execution 249ms | |
| parsing 56.2ms | |
| type checking 7.86ms | |
| src/category_theory/category/Rel.lean | |
| cumulative profiling times: | |
| compilation 6.13ms | |
| decl post-processing 5.72ms | |
| elaboration 2.24s | |
| elaboration: tactic compilation 131ms | |
| elaboration: tactic execution 2.02s | |
| parsing 13.9ms | |
| type checking 2.54ms | |
| src/category_theory/category/default.lean | |
| cumulative profiling times: | |
| compilation 20ms | |
| decl post-processing 30.4ms | |
| elaboration 4.08s | |
| elaboration: tactic compilation 352ms | |
| elaboration: tactic execution 2.73s | |
| parsing 686ms | |
| type checking 28.2ms | |
| src/category_theory/comma.lean | |
| cumulative profiling times: | |
| compilation 735ms | |
| decl post-processing 3.22s | |
| elaboration 224s | |
| elaboration: tactic compilation 566ms | |
| elaboration: tactic execution 221s | |
| parsing 808ms | |
| type checking 1.8s | |
| src/category_theory/concrete_category/basic.lean | |
| cumulative profiling times: | |
| compilation 30.4ms | |
| decl post-processing 51.1ms | |
| elaboration 724ms | |
| elaboration: tactic compilation 49.1ms | |
| elaboration: tactic execution 401ms | |
| parsing 104ms | |
| type checking 28.4ms | |
| src/category_theory/concrete_category/bundled.lean | |
| cumulative profiling times: | |
| compilation 3.21ms | |
| decl post-processing 3.92ms | |
| elaboration 3.65ms | |
| parsing 1.06ms | |
| type checking 1.76ms | |
| src/category_theory/concrete_category/bundled_hom.lean | |
| cumulative profiling times: | |
| compilation 53.9ms | |
| decl post-processing 80.6ms | |
| elaboration 1.99s | |
| elaboration: tactic compilation 60.1ms | |
| elaboration: tactic execution 1.54s | |
| parsing 60.5ms | |
| type checking 47.8ms | |
| src/category_theory/concrete_category/default.lean | |
| src/category_theory/concrete_category/unbundled_hom.lean | |
| cumulative profiling times: | |
| compilation 21.3ms | |
| decl post-processing 24.8ms | |
| elaboration 146ms | |
| elaboration: tactic compilation 34.9ms | |
| elaboration: tactic execution 0ms | |
| parsing 11.1ms | |
| type checking 13.3ms | |
| src/category_theory/conj.lean | |
| cumulative profiling times: | |
| compilation 20.6ms | |
| decl post-processing 38.6ms | |
| elaboration 2.67s | |
| elaboration: tactic compilation 163ms | |
| elaboration: tactic execution 1.09s | |
| parsing 279ms | |
| type checking 46.7ms | |
| src/category_theory/connected.lean | |
| cumulative profiling times: | |
| compilation 21.4ms | |
| decl post-processing 25.4ms | |
| elaboration 5.97s | |
| elaboration: tactic compilation 162ms | |
| elaboration: tactic execution 4.66s | |
| parsing 354ms | |
| type checking 16.4ms | |
| src/category_theory/const.lean | |
| cumulative profiling times: | |
| compilation 63.7ms | |
| decl post-processing 149ms | |
| elaboration 12.4s | |
| elaboration: tactic compilation 6.87ms | |
| elaboration: tactic execution 11.3s | |
| parsing 3.46ms | |
| type checking 100ms | |
| src/category_theory/core.lean | |
| cumulative profiling times: | |
| compilation 79.3ms | |
| decl post-processing 58ms | |
| elaboration 6.96s | |
| elaboration: tactic compilation 57.4ms | |
| elaboration: tactic execution 6.13s | |
| parsing 67.1ms | |
| type checking 40.1ms | |
| src/category_theory/currying.lean | |
| cumulative profiling times: | |
| compilation 238ms | |
| decl post-processing 1s | |
| elaboration 34.9s | |
| elaboration: tactic compilation 165ms | |
| elaboration: tactic execution 31.1s | |
| parsing 269ms | |
| type checking 890ms | |
| src/category_theory/differential_object.lean | |
| cumulative profiling times: | |
| compilation 71.5ms | |
| decl post-processing 145ms | |
| elaboration 26.7s | |
| elaboration: tactic compilation 30.9ms | |
| elaboration: tactic execution 24.9s | |
| parsing 42.7ms | |
| type checking 68.9ms | |
| src/category_theory/discrete_category.lean | |
| cumulative profiling times: | |
| compilation 56.6ms | |
| decl post-processing 74.5ms | |
| elaboration 14.7s | |
| elaboration: tactic compilation 208ms | |
| elaboration: tactic execution 13.2s | |
| parsing 262ms | |
| type checking 48.8ms | |
| src/category_theory/elements.lean | |
| cumulative profiling times: | |
| compilation 185ms | |
| decl post-processing 397ms | |
| elaboration 82.7s | |
| elaboration: tactic compilation 129ms | |
| elaboration: tactic execution 78.1s | |
| parsing 82.5ms | |
| type checking 414ms | |
| src/category_theory/endomorphism.lean | |
| cumulative profiling times: | |
| compilation 35.7ms | |
| decl post-processing 49.5ms | |
| elaboration 1.7s | |
| elaboration: tactic compilation 26.7ms | |
| elaboration: tactic execution 1.32s | |
| parsing 35.4ms | |
| type checking 25.5ms | |
| src/category_theory/epi_mono.lean | |
| cumulative profiling times: | |
| compilation 44.4ms | |
| decl post-processing 198ms | |
| elaboration 3.58s | |
| elaboration: tactic compilation 152ms | |
| elaboration: tactic execution 2.61s | |
| parsing 382ms | |
| type checking 43.6ms | |
| src/category_theory/eq_to_hom.lean | |
| cumulative profiling times: | |
| compilation 7.22ms | |
| decl post-processing 55.2ms | |
| elaboration 5.93s | |
| elaboration: tactic compilation 196ms | |
| elaboration: tactic execution 5.06s | |
| parsing 373ms | |
| type checking 13.3ms | |
| src/category_theory/equivalence.lean | |
| cumulative profiling times: | |
| compilation 229ms | |
| decl post-processing 327ms | |
| elaboration 16.1s | |
| elaboration: tactic compilation 433ms | |
| elaboration: tactic execution 12.5s | |
| parsing 1.12s | |
| type checking 324ms | |
| src/category_theory/full_subcategory.lean | |
| cumulative profiling times: | |
| compilation 22.2ms | |
| decl post-processing 36.9ms | |
| elaboration 1.09s | |
| elaboration: tactic compilation 2.26ms | |
| elaboration: tactic execution 882ms | |
| parsing 1.88ms | |
| type checking 22.8ms | |
| src/category_theory/fully_faithful.lean | |
| cumulative profiling times: | |
| compilation 40.9ms | |
| decl post-processing 65.7ms | |
| elaboration 4.81s | |
| elaboration: tactic compilation 194ms | |
| elaboration: tactic execution 3.6s | |
| parsing 355ms | |
| type checking 41.4ms | |
| src/category_theory/functor.lean | |
| cumulative profiling times: | |
| compilation 21ms | |
| decl post-processing 21.9ms | |
| elaboration 636ms | |
| elaboration: tactic compilation 25.2ms | |
| elaboration: tactic execution 360ms | |
| parsing 21.2ms | |
| type checking 15.3ms | |
| src/category_theory/functor_category.lean | |
| cumulative profiling times: | |
| compilation 45.1ms | |
| decl post-processing 101ms | |
| elaboration 5.07s | |
| elaboration: tactic compilation 67.7ms | |
| elaboration: tactic execution 4.29s | |
| parsing 107ms | |
| type checking 107ms | |
| src/category_theory/functorial.lean | |
| cumulative profiling times: | |
| compilation 24.1ms | |
| decl post-processing 22.5ms | |
| elaboration 79.5ms | |
| elaboration: tactic compilation 0.67ms | |
| elaboration: tactic execution 4ms | |
| parsing 1.17ms | |
| type checking 11.2ms | |
| src/category_theory/graded_object.lean | |
| cumulative profiling times: | |
| compilation 121ms | |
| decl post-processing 325ms | |
| elaboration 87.2s | |
| elaboration: tactic compilation 191ms | |
| elaboration: tactic execution 80.2s | |
| parsing 371ms | |
| type checking 104ms | |
| src/category_theory/groupoid.lean | |
| cumulative profiling times: | |
| compilation 27ms | |
| decl post-processing 25.7ms | |
| elaboration 2.33s | |
| elaboration: tactic compilation 18.4ms | |
| elaboration: tactic execution 1.96s | |
| parsing 15.5ms | |
| type checking 14.2ms | |
| src/category_theory/hom_functor.lean | |
| cumulative profiling times: | |
| compilation 10.9ms | |
| decl post-processing 9.58ms | |
| elaboration 3.32s | |
| elaboration: tactic compilation 0.776ms | |
| elaboration: tactic execution 3.09s | |
| parsing 0.683ms | |
| type checking 8.9ms | |
| src/category_theory/isomorphism.lean | |
| cumulative profiling times: | |
| compilation 48.1ms | |
| decl post-processing 120ms | |
| elaboration 4.26s | |
| elaboration: tactic compilation 370ms | |
| elaboration: tactic execution 2.63s | |
| parsing 519ms | |
| type checking 58.7ms | |
| src/category_theory/isomorphism_classes.lean | |
| cumulative profiling times: | |
| compilation 8.02ms | |
| decl post-processing 8.59ms | |
| elaboration 1.58s | |
| elaboration: tactic compilation 0.839ms | |
| elaboration: tactic execution 1.42s | |
| parsing 1.71ms | |
| type checking 4.67ms | |
| src/category_theory/limits/concrete_category.lean | |
| cumulative profiling times: | |
| compilation 0.006ms | |
| decl post-processing 5.26ms | |
| elaboration 3.14s | |
| elaboration: tactic compilation 35.4ms | |
| elaboration: tactic execution 2.92s | |
| parsing 122ms | |
| type checking 7.45ms | |
| src/category_theory/limits/cones.lean | |
| cumulative profiling times: | |
| compilation 544ms | |
| decl post-processing 1.48s | |
| elaboration 61.5s | |
| elaboration: tactic compilation 422ms | |
| elaboration: tactic execution 54.7s | |
| parsing 640ms | |
| type checking 658ms | |
| src/category_theory/limits/connected.lean | |
| cumulative profiling times: | |
| compilation 73.7ms | |
| decl post-processing 135ms | |
| elaboration 18.5s | |
| elaboration: tactic compilation 122ms | |
| elaboration: tactic execution 16.2s | |
| parsing 186ms | |
| type checking 31.4ms | |
| src/category_theory/limits/creates.lean | |
| cumulative profiling times: | |
| compilation 305ms | |
| decl post-processing 290ms | |
| elaboration 4.98s | |
| elaboration: tactic compilation 150ms | |
| elaboration: tactic execution 3.8s | |
| parsing 507ms | |
| type checking 120ms | |
| src/category_theory/limits/functor_category.lean | |
| cumulative profiling times: | |
| compilation 158ms | |
| decl post-processing 389ms | |
| elaboration 29.9s | |
| elaboration: tactic compilation 136ms | |
| elaboration: tactic execution 27.3s | |
| parsing 166ms | |
| type checking 248ms | |
| src/category_theory/limits/lattice.lean | |
| cumulative profiling times: | |
| compilation 59.5ms | |
| decl post-processing 66.9ms | |
| elaboration 1.6s | |
| elaboration: tactic compilation 82.9ms | |
| elaboration: tactic execution 2.45s | |
| parsing 22.7ms | |
| type checking 45.7ms | |
| src/category_theory/limits/limits.lean | |
| cumulative profiling times: | |
| compilation 610ms | |
| decl post-processing 1.75s | |
| elaboration 114s | |
| elaboration: tactic compilation 1.52s | |
| elaboration: tactic execution 102s | |
| parsing 3.55s | |
| type checking 786ms | |
| src/category_theory/limits/opposites.lean | |
| cumulative profiling times: | |
| compilation 36.7ms | |
| decl post-processing 45.1ms | |
| elaboration 1.86s | |
| elaboration: tactic compilation 149ms | |
| elaboration: tactic execution 637ms | |
| parsing 352ms | |
| type checking 16.3ms | |
| src/category_theory/limits/over.lean | |
| cumulative profiling times: | |
| compilation 868ms | |
| decl post-processing 2.34s | |
| elaboration 186s | |
| elaboration: tactic compilation 496ms | |
| elaboration: tactic execution 170s | |
| parsing 593ms | |
| type checking 1.44s | |
| src/category_theory/limits/preserves.lean | |
| cumulative profiling times: | |
| compilation 223ms | |
| decl post-processing 453ms | |
| elaboration 6.91s | |
| elaboration: tactic compilation 485ms | |
| elaboration: tactic execution 5.49s | |
| parsing 561ms | |
| type checking 277ms | |
| src/category_theory/limits/shapes/binary_products.lean | |
| cumulative profiling times: | |
| compilation 407ms | |
| decl post-processing 2.02s | |
| elaboration 290s | |
| elaboration: tactic compilation 318ms | |
| elaboration: tactic execution 275s | |
| parsing 346ms | |
| type checking 460ms | |
| src/category_theory/limits/shapes/biproducts.lean | |
| cumulative profiling times: | |
| compilation 173ms | |
| decl post-processing 125ms | |
| elaboration 11.5s | |
| elaboration: tactic compilation 22.4ms | |
| elaboration: tactic execution 10.1s | |
| parsing 8.18ms | |
| type checking 68.7ms | |
| src/category_theory/limits/shapes/constructions/binary_products.lean | |
| cumulative profiling times: | |
| compilation 141ms | |
| decl post-processing 45.6ms | |
| elaboration 982ms | |
| elaboration: tactic compilation 18.9ms | |
| elaboration: tactic execution 649ms | |
| parsing 66.8ms | |
| type checking 12.2ms | |
| src/category_theory/limits/shapes/constructions/equalizers.lean | |
| cumulative profiling times: | |
| compilation 68.7ms | |
| decl post-processing 42.6ms | |
| elaboration 15.2s | |
| elaboration: tactic compilation 107ms | |
| elaboration: tactic execution 13.8s | |
| parsing 358ms | |
| type checking 28.8ms | |
| src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean | |
| cumulative profiling times: | |
| compilation 147ms | |
| decl post-processing 179ms | |
| elaboration 66.6s | |
| elaboration: tactic compilation 137ms | |
| elaboration: tactic execution 61.9s | |
| parsing 572ms | |
| type checking 91.6ms | |
| src/category_theory/limits/shapes/constructions/pullbacks.lean | |
| cumulative profiling times: | |
| compilation 105ms | |
| decl post-processing 154ms | |
| elaboration 21.1s | |
| elaboration: tactic compilation 252ms | |
| elaboration: tactic execution 18.6s | |
| parsing 605ms | |
| type checking 113ms | |
| src/category_theory/limits/shapes/default.lean | |
| src/category_theory/limits/shapes/equalizers.lean | |
| cumulative profiling times: | |
| compilation 478ms | |
| decl post-processing 1.37s | |
| elaboration 76s | |
| elaboration: tactic compilation 728ms | |
| elaboration: tactic execution 74.2s | |
| parsing 1.12s | |
| type checking 359ms | |
| src/category_theory/limits/shapes/finite_limits.lean | |
| cumulative profiling times: | |
| compilation 12.4ms | |
| decl post-processing 10.4ms | |
| elaboration 490ms | |
| elaboration: tactic compilation 26.6ms | |
| elaboration: tactic execution 222ms | |
| parsing 1.09ms | |
| type checking 1.78ms | |
| src/category_theory/limits/shapes/finite_products.lean | |
| cumulative profiling times: | |
| compilation 12ms | |
| decl post-processing 9.91ms | |
| elaboration 1.24s | |
| elaboration: tactic compilation 59.6ms | |
| elaboration: tactic execution 841ms | |
| parsing 1.01ms | |
| type checking 1.45ms | |
| src/category_theory/limits/shapes/images.lean | |
| cumulative profiling times: | |
| compilation 259ms | |
| decl post-processing 2.54s | |
| elaboration 89.2s | |
| elaboration: tactic compilation 594ms | |
| elaboration: tactic execution 90.6s | |
| parsing 1.23s | |
| type checking 205ms | |
| src/category_theory/limits/shapes/kernels.lean | |
| cumulative profiling times: | |
| compilation 210ms | |
| decl post-processing 914ms | |
| elaboration 12.8s | |
| elaboration: tactic compilation 150ms | |
| elaboration: tactic execution 11s | |
| parsing 257ms | |
| type checking 121ms | |
| src/category_theory/limits/shapes/products.lean | |
| cumulative profiling times: | |
| compilation 40.9ms | |
| decl post-processing 16.8ms | |
| elaboration 8.91s | |
| elaboration: tactic compilation 0.879ms | |
| elaboration: tactic execution 8.34s | |
| parsing 3.8ms | |
| type checking 29.2ms | |
| src/category_theory/limits/shapes/pullbacks.lean | |
| cumulative profiling times: | |
| compilation 317ms | |
| decl post-processing 3.02s | |
| elaboration 89.1s | |
| elaboration: tactic compilation 353ms | |
| elaboration: tactic execution 83.3s | |
| parsing 253ms | |
| type checking 328ms | |
| src/category_theory/limits/shapes/regular_mono.lean | |
| cumulative profiling times: | |
| compilation 96.6ms | |
| decl post-processing 104ms | |
| elaboration 7.97s | |
| elaboration: tactic compilation 103ms | |
| elaboration: tactic execution 7.48s | |
| parsing 175ms | |
| type checking 50.8ms | |
| src/category_theory/limits/shapes/strong_epi.lean | |
| cumulative profiling times: | |
| compilation 45.9ms | |
| decl post-processing 71.3ms | |
| elaboration 6.82s | |
| elaboration: tactic compilation 117ms | |
| elaboration: tactic execution 8.8s | |
| parsing 361ms | |
| type checking 48.4ms | |
| src/category_theory/limits/shapes/terminal.lean | |
| cumulative profiling times: | |
| compilation 100ms | |
| decl post-processing 49ms | |
| elaboration 6.87s | |
| elaboration: tactic compilation 85.9ms | |
| elaboration: tactic execution 5.97s | |
| parsing 29.7ms | |
| type checking 45ms | |
| src/category_theory/limits/shapes/wide_pullbacks.lean | |
| cumulative profiling times: | |
| compilation 739ms | |
| decl post-processing 336ms | |
| elaboration 92.9s | |
| elaboration: tactic compilation 417ms | |
| elaboration: tactic execution 85.5s | |
| parsing 243ms | |
| type checking 130ms | |
| src/category_theory/limits/shapes/zero.lean | |
| cumulative profiling times: | |
| compilation 66.5ms | |
| decl post-processing 107ms | |
| elaboration 14.1s | |
| elaboration: tactic compilation 319ms | |
| elaboration: tactic execution 12.6s | |
| parsing 417ms | |
| type checking 26.5ms | |
| src/category_theory/limits/types.lean | |
| cumulative profiling times: | |
| compilation 76.6ms | |
| decl post-processing 103ms | |
| elaboration 20.2s | |
| elaboration: tactic compilation 131ms | |
| elaboration: tactic execution 25.2s | |
| parsing 231ms | |
| type checking 125ms | |
| src/category_theory/monad/adjunction.lean | |
| cumulative profiling times: | |
| compilation 153ms | |
| decl post-processing 306ms | |
| elaboration 27.7s | |
| elaboration: tactic compilation 261ms | |
| elaboration: tactic execution 24.5s | |
| parsing 535ms | |
| type checking 274ms | |
| src/category_theory/monad/algebra.lean | |
| cumulative profiling times: | |
| compilation 215ms | |
| decl post-processing 662ms | |
| elaboration 44.7s | |
| elaboration: tactic compilation 233ms | |
| elaboration: tactic execution 40.6s | |
| parsing 471ms | |
| type checking 360ms | |
| src/category_theory/monad/basic.lean | |
| src/category_theory/monad/default.lean | |
| src/category_theory/monad/limits.lean | |
| cumulative profiling times: | |
| compilation 303ms | |
| decl post-processing 763ms | |
| elaboration 34.3s | |
| elaboration: tactic compilation 321ms | |
| elaboration: tactic execution 29.9s | |
| parsing 902ms | |
| type checking 277ms | |
| src/category_theory/monad/types.lean | |
| cumulative profiling times: | |
| compilation 12.6ms | |
| decl post-processing 15.3ms | |
| elaboration 39.8ms | |
| parsing 0.757ms | |
| type checking 14.5ms | |
| src/category_theory/monoidal/category.lean | |
| cumulative profiling times: | |
| compilation 121ms | |
| decl post-processing 114ms | |
| elaboration 19.8s | |
| elaboration: tactic compilation 730ms | |
| elaboration: tactic execution 15.8s | |
| parsing 1.66s | |
| type checking 104ms | |
| src/category_theory/monoidal/functor.lean | |
| cumulative profiling times: | |
| compilation 168ms | |
| decl post-processing 311ms | |
| elaboration 8.04s | |
| elaboration: tactic compilation 200ms | |
| elaboration: tactic execution 6.41s | |
| parsing 273ms | |
| type checking 124ms | |
| src/category_theory/monoidal/functorial.lean | |
| cumulative profiling times: | |
| compilation 58.1ms | |
| decl post-processing 59.9ms | |
| elaboration 2.41s | |
| elaboration: tactic compilation 1.4ms | |
| elaboration: tactic execution 2.05s | |
| parsing 0.606ms | |
| type checking 49.7ms | |
| src/category_theory/monoidal/of_has_finite_products.lean | |
| cumulative profiling times: | |
| compilation 38.2ms | |
| decl post-processing 58.8ms | |
| elaboration 42.6s | |
| elaboration: tactic compilation 30.5ms | |
| elaboration: tactic execution 40.1s | |
| parsing 2.81ms | |
| type checking 75.8ms | |
| src/category_theory/monoidal/types.lean | |
| cumulative profiling times: | |
| compilation 1.06ms | |
| decl post-processing 1.64ms | |
| elaboration 39.4ms | |
| elaboration: tactic compilation 11.6ms | |
| elaboration: tactic execution 0ms | |
| parsing 0.352ms | |
| type checking 0.332ms | |
| src/category_theory/natural_isomorphism.lean | |
| cumulative profiling times: | |
| compilation 95.2ms | |
| decl post-processing 130ms | |
| elaboration 9.13s | |
| elaboration: tactic compilation 172ms | |
| elaboration: tactic execution 7.47s | |
| parsing 319ms | |
| type checking 101ms | |
| src/category_theory/natural_transformation.lean | |
| cumulative profiling times: | |
| compilation 17ms | |
| decl post-processing 12.6ms | |
| elaboration 649ms | |
| elaboration: tactic compilation 12.7ms | |
| elaboration: tactic execution 611ms | |
| parsing 19.6ms | |
| type checking 7.39ms | |
| src/category_theory/opposites.lean | |
| cumulative profiling times: | |
| compilation 147ms | |
| decl post-processing 424ms | |
| elaboration 15.8s | |
| elaboration: tactic compilation 209ms | |
| elaboration: tactic execution 13.2s | |
| parsing 528ms | |
| type checking 209ms | |
| src/category_theory/pempty.lean | |
| cumulative profiling times: | |
| compilation 70.3ms | |
| decl post-processing 33.7ms | |
| elaboration 14s | |
| elaboration: tactic compilation 224ms | |
| elaboration: tactic execution 12.9s | |
| parsing 25.2ms | |
| type checking 12.8ms | |
| src/category_theory/products/associator.lean | |
| cumulative profiling times: | |
| compilation 54.8ms | |
| decl post-processing 190ms | |
| elaboration 5.55s | |
| elaboration: tactic compilation 65.5ms | |
| elaboration: tactic execution 4.83s | |
| parsing 56.2ms | |
| type checking 77.8ms | |
| src/category_theory/products/basic.lean | |
| cumulative profiling times: | |
| compilation 151ms | |
| decl post-processing 496ms | |
| elaboration 23s | |
| elaboration: tactic compilation 117ms | |
| elaboration: tactic execution 20.7s | |
| parsing 184ms | |
| type checking 170ms | |
| src/category_theory/products/bifunctor.lean | |
| cumulative profiling times: | |
| compilation 0.0202ms | |
| decl post-processing 16.4ms | |
| elaboration 263ms | |
| elaboration: tactic compilation 58.1ms | |
| elaboration: tactic execution 69ms | |
| parsing 87.7ms | |
| type checking 18.5ms | |
| src/category_theory/products/default.lean | |
| src/category_theory/punit.lean | |
| cumulative profiling times: | |
| compilation 5.39ms | |
| decl post-processing 6.02ms | |
| elaboration 195ms | |
| elaboration: tactic compilation 21.8ms | |
| elaboration: tactic execution 112ms | |
| parsing 0.537ms | |
| type checking 3.22ms | |
| src/category_theory/quotient.lean | |
| cumulative profiling times: | |
| compilation 60ms | |
| decl post-processing 135ms | |
| elaboration 4.95s | |
| elaboration: tactic compilation 120ms | |
| elaboration: tactic execution 4.01s | |
| parsing 154ms | |
| type checking 65.7ms | |
| src/category_theory/reflect_isomorphisms.lean | |
| cumulative profiling times: | |
| compilation 60.1ms | |
| decl post-processing 71.7ms | |
| elaboration 6.93s | |
| elaboration: tactic compilation 33.6ms | |
| elaboration: tactic execution 6.23s | |
| parsing 133ms | |
| type checking 45.5ms | |
| src/category_theory/shift.lean | |
| cumulative profiling times: | |
| compilation 0.866ms | |
| decl post-processing 2.7ms | |
| elaboration 42.3ms | |
| elaboration: tactic compilation 10.3ms | |
| elaboration: tactic execution 3ms | |
| parsing 3.5ms | |
| type checking 0.984ms | |
| src/category_theory/single_obj.lean | |
| cumulative profiling times: | |
| compilation 65.6ms | |
| decl post-processing 115ms | |
| elaboration 16.8s | |
| elaboration: tactic compilation 48.4ms | |
| elaboration: tactic execution 14.9s | |
| parsing 17.6ms | |
| type checking 81.6ms | |
| src/category_theory/sparse.lean | |
| cumulative profiling times: | |
| compilation 2.27ms | |
| decl post-processing 2.54ms | |
| elaboration 334ms | |
| elaboration: tactic compilation 37ms | |
| elaboration: tactic execution 261ms | |
| parsing 0.747ms | |
| type checking 1.21ms | |
| src/category_theory/sums/associator.lean | |
| cumulative profiling times: | |
| compilation 171ms | |
| decl post-processing 44.6ms | |
| elaboration 10.7s | |
| elaboration: tactic compilation 279ms | |
| elaboration: tactic execution 9.6s | |
| parsing 30.1ms | |
| type checking 47.5ms | |
| src/category_theory/sums/basic.lean | |
| cumulative profiling times: | |
| compilation 151ms | |
| decl post-processing 96.4ms | |
| elaboration 10.1s | |
| elaboration: tactic compilation 293ms | |
| elaboration: tactic execution 8.43s | |
| parsing 147ms | |
| type checking 66.1ms | |
| src/category_theory/sums/default.lean | |
| src/category_theory/types.lean | |
| cumulative profiling times: | |
| compilation 35.6ms | |
| decl post-processing 60.3ms | |
| elaboration 8.5s | |
| elaboration: tactic compilation 225ms | |
| elaboration: tactic execution 7.94s | |
| parsing 492ms | |
| type checking 43.9ms | |
| src/category_theory/whiskering.lean | |
| cumulative profiling times: | |
| compilation 186ms | |
| decl post-processing 856ms | |
| elaboration 15.6s | |
| elaboration: tactic compilation 139ms | |
| elaboration: tactic execution 13.2s | |
| parsing 300ms | |
| type checking 690ms | |
| src/category_theory/yoneda.lean | |
| cumulative profiling times: | |
| compilation 160ms | |
| decl post-processing 416ms | |
| elaboration 30.8s | |
| elaboration: tactic compilation 281ms | |
| elaboration: tactic execution 27.2s | |
| parsing 739ms | |
| type checking 294ms | |
| src/combinatorics/composition.lean | |
| cumulative profiling times: | |
| compilation 134ms | |
| decl post-processing 92.9ms | |
| elaboration 123s | |
| elaboration: tactic compilation 1.93s | |
| elaboration: tactic execution 113s | |
| parsing 6.48s | |
| type checking 56.4ms | |
| src/computability/halting.lean | |
| cumulative profiling times: | |
| compilation 1.6ms | |
| decl post-processing 8.76ms | |
| elaboration 25.7s | |
| elaboration: tactic compilation 982ms | |
| elaboration: tactic execution 21.5s | |
| parsing 2.38s | |
| type checking 23.4ms | |
| src/computability/partrec.lean | |
| cumulative profiling times: | |
| compilation 25.4ms | |
| decl post-processing 30.8ms | |
| elaboration 47.7s | |
| elaboration: tactic compilation 1.23s | |
| elaboration: tactic execution 38.9s | |
| parsing 3.71s | |
| type checking 42.2ms | |
| src/computability/partrec_code.lean | |
| cumulative profiling times: | |
| compilation 63.8ms | |
| decl post-processing 64.8ms | |
| elaboration 91s | |
| elaboration: tactic compilation 2s | |
| elaboration: tactic execution 78.9s | |
| parsing 10.5s | |
| type checking 20.3ms | |
| src/computability/primrec.lean | |
| cumulative profiling times: | |
| compilation 51.4ms | |
| decl post-processing 58.5ms | |
| elaboration 59.3s | |
| elaboration: tactic compilation 3.02s | |
| elaboration: tactic execution 44.3s | |
| parsing 8.45s | |
| type checking 83.8ms | |
| src/computability/reduce.lean | |
| cumulative profiling times: | |
| compilation 40ms | |
| decl post-processing 63.8ms | |
| elaboration 10.1s | |
| elaboration: tactic compilation 185ms | |
| elaboration: tactic execution 10.7s | |
| parsing 353ms | |
| type checking 29.6ms | |
| src/computability/turing_machine.lean | |
| cumulative profiling times: | |
| compilation 277ms | |
| decl post-processing 1.02s | |
| elaboration 106s | |
| elaboration: tactic compilation 4.19s | |
| elaboration: tactic execution 69.4s | |
| parsing 12.1s | |
| type checking 169ms | |
| src/control/applicative.lean | |
| cumulative profiling times: | |
| compilation 43.6ms | |
| decl post-processing 190ms | |
| elaboration 3.75s | |
| elaboration: tactic compilation 221ms | |
| elaboration: tactic execution 2.32s | |
| parsing 489ms | |
| type checking 118ms | |
| src/control/basic.lean | |
| cumulative profiling times: | |
| compilation 35.8ms | |
| decl post-processing 131ms | |
| elaboration 2.9s | |
| elaboration: tactic compilation 294ms | |
| elaboration: tactic execution 1.36s | |
| parsing 461ms | |
| type checking 76.9ms | |
| src/control/bifunctor.lean | |
| cumulative profiling times: | |
| compilation 39.3ms | |
| decl post-processing 79ms | |
| elaboration 2.11s | |
| elaboration: tactic compilation 144ms | |
| elaboration: tactic execution 1.44s | |
| parsing 211ms | |
| type checking 16.5ms | |
| src/control/bitraversable/basic.lean | |
| cumulative profiling times: | |
| compilation 1.92ms | |
| decl post-processing 1.58ms | |
| elaboration 0.813ms | |
| parsing 0.141ms | |
| type checking 0.156ms | |
| src/control/bitraversable/instances.lean | |
| cumulative profiling times: | |
| compilation 71.1ms | |
| decl post-processing 57.6ms | |
| elaboration 7.05s | |
| elaboration: tactic compilation 130ms | |
| elaboration: tactic execution 5.8s | |
| parsing 285ms | |
| type checking 18.1ms | |
| src/control/bitraversable/lemmas.lean | |
| cumulative profiling times: | |
| compilation 8.18ms | |
| decl post-processing 115ms | |
| elaboration 1.77s | |
| elaboration: tactic compilation 91.4ms | |
| elaboration: tactic execution 1.33s | |
| parsing 209ms | |
| type checking 7.13ms | |
| src/control/equiv_functor.lean | |
| cumulative profiling times: | |
| compilation 6ms | |
| decl post-processing 5.98ms | |
| elaboration 738ms | |
| elaboration: tactic compilation 52.6ms | |
| elaboration: tactic execution 411ms | |
| parsing 127ms | |
| type checking 2.3ms | |
| src/control/equiv_functor/instances.lean | |
| cumulative profiling times: | |
| compilation 3.91ms | |
| decl post-processing 9.11ms | |
| elaboration 1.17s | |
| elaboration: tactic compilation 10.4ms | |
| elaboration: tactic execution 1.02s | |
| parsing 0.438ms | |
| type checking 8.41ms | |
| src/control/fold.lean | |
| cumulative profiling times: | |
| compilation 61.4ms | |
| decl post-processing 124ms | |
| elaboration 6.43s | |
| elaboration: tactic compilation 587ms | |
| elaboration: tactic execution 3.31s | |
| parsing 1.33s | |
| type checking 67ms | |
| src/control/functor.lean | |
| cumulative profiling times: | |
| compilation 18.1ms | |
| decl post-processing 34.6ms | |
| elaboration 856ms | |
| elaboration: tactic compilation 92.9ms | |
| elaboration: tactic execution 494ms | |
| parsing 165ms | |
| type checking 10.6ms | |
| src/control/monad/basic.lean | |
| cumulative profiling times: | |
| compilation 0.0023ms | |
| decl post-processing 0.0356ms | |
| elaboration 25.6ms | |
| elaboration: tactic compilation 12.1ms | |
| elaboration: tactic execution 0ms | |
| parsing 16.2ms | |
| type checking 0.334ms | |
| src/control/monad/cont.lean | |
| cumulative profiling times: | |
| compilation 92.6ms | |
| decl post-processing 218ms | |
| elaboration 4.81s | |
| elaboration: tactic compilation 433ms | |
| elaboration: tactic execution 2s | |
| parsing 800ms | |
| type checking 97.9ms | |
| src/control/monad/writer.lean | |
| cumulative profiling times: | |
| compilation 181ms | |
| decl post-processing 564ms | |
| elaboration 1.35s | |
| elaboration: tactic compilation 61.4ms | |
| elaboration: tactic execution 396ms | |
| parsing 113ms | |
| type checking 329ms | |
| src/control/traversable/basic.lean | |
| cumulative profiling times: | |
| compilation 21.8ms | |
| decl post-processing 14.1ms | |
| elaboration 362ms | |
| elaboration: tactic compilation 25.5ms | |
| elaboration: tactic execution 224ms | |
| parsing 36.2ms | |
| type checking 7.52ms | |
| src/control/traversable/default.lean | |
| src/control/traversable/derive.lean | |
| cumulative profiling times: | |
| compilation 1.22s | |
| decl post-processing 0.331ms | |
| elaboration 1.86s | |
| parsing 46.6ms | |
| type checking 41.2ms | |
| src/control/traversable/equiv.lean | |
| cumulative profiling times: | |
| compilation 27.3ms | |
| decl post-processing 33ms | |
| elaboration 5.49s | |
| elaboration: tactic compilation 220ms | |
| elaboration: tactic execution 4.08s | |
| parsing 879ms | |
| type checking 17.8ms | |
| src/control/traversable/instances.lean | |
| cumulative profiling times: | |
| compilation 15.4ms | |
| decl post-processing 13.3ms | |
| elaboration 19.9s | |
| elaboration: tactic compilation 356ms | |
| elaboration: tactic execution 17.2s | |
| parsing 748ms | |
| type checking 21.2ms | |
| src/control/traversable/lemmas.lean | |
| cumulative profiling times: | |
| compilation 6.05ms | |
| decl post-processing 2.71ms | |
| elaboration 2.52s | |
| elaboration: tactic compilation 211ms | |
| elaboration: tactic execution 1.53s | |
| parsing 511ms | |
| type checking 10.3ms | |
| src/data/W.lean | |
| cumulative profiling times: | |
| compilation 34ms | |
| decl post-processing 60ms | |
| elaboration 673ms | |
| elaboration: tactic compilation 74.2ms | |
| elaboration: tactic execution 30ms | |
| parsing 232ms | |
| type checking 8.32ms | |
| src/data/analysis/filter.lean | |
| cumulative profiling times: | |
| compilation 163ms | |
| decl post-processing 108ms | |
| elaboration 29s | |
| elaboration: tactic compilation 303ms | |
| elaboration: tactic execution 27.7s | |
| parsing 581ms | |
| type checking 56ms | |
| src/data/analysis/topology.lean | |
| cumulative profiling times: | |
| compilation 44.7ms | |
| decl post-processing 54.8ms | |
| elaboration 32.8s | |
| elaboration: tactic compilation 187ms | |
| elaboration: tactic execution 29.8s | |
| parsing 549ms | |
| type checking 27.9ms | |
| src/data/array/lemmas.lean | |
| cumulative profiling times: | |
| compilation 15.3ms | |
| decl post-processing 22.4ms | |
| elaboration 13.3s | |
| elaboration: tactic compilation 464ms | |
| elaboration: tactic execution 11.1s | |
| parsing 1.2s | |
| type checking 15.6ms | |
| src/data/bool.lean | |
| cumulative profiling times: | |
| compilation 4.66ms | |
| decl post-processing 9.6ms | |
| elaboration 3.06s | |
| elaboration: tactic compilation 457ms | |
| elaboration: tactic execution 1.03s | |
| parsing 308ms | |
| type checking 4.5ms | |
| src/data/buffer/basic.lean | |
| cumulative profiling times: | |
| compilation 20ms | |
| decl post-processing 30.9ms | |
| elaboration 6.14s | |
| elaboration: tactic compilation 113ms | |
| elaboration: tactic execution 5.2s | |
| parsing 417ms | |
| type checking 3.53ms | |
| src/data/char.lean | |
| cumulative profiling times: | |
| compilation 5.81ms | |
| decl post-processing 6.04ms | |
| elaboration 21.3ms | |
| parsing 0.323ms | |
| type checking 5.51ms | |
| src/data/complex/basic.lean | |
| cumulative profiling times: | |
| compilation 70.3ms | |
| decl post-processing 662ms | |
| elaboration 192s | |
| elaboration: tactic compilation 2.14s | |
| elaboration: tactic execution 186s | |
| parsing 3.49s | |
| type checking 210ms | |
| src/data/complex/exponential.lean | |
| cumulative profiling times: | |
| compilation 0.697ms | |
| decl post-processing 45.2ms | |
| elaboration 220s | |
| elaboration: tactic compilation 4.68s | |
| elaboration: tactic execution 201s | |
| parsing 9.1s | |
| type checking 51.5ms | |
| src/data/complex/module.lean | |
| cumulative profiling times: | |
| compilation 0.0138ms | |
| decl post-processing 41.5ms | |
| elaboration 414ms | |
| parsing 0.597ms | |
| type checking 39.9ms | |
| src/data/dfinsupp.lean | |
| cumulative profiling times: | |
| compilation 503ms | |
| decl post-processing 44s | |
| elaboration 254s | |
| elaboration: tactic compilation 3.2s | |
| elaboration: tactic execution 221s | |
| parsing 8.64s | |
| type checking 796ms | |
| src/data/dlist/basic.lean | |
| cumulative profiling times: | |
| compilation 0.27ms | |
| decl post-processing 2.19ms | |
| elaboration 17.3ms | |
| parsing 0.457ms | |
| type checking 0.0333ms | |
| src/data/dlist/instances.lean | |
| cumulative profiling times: | |
| compilation 5.15ms | |
| decl post-processing 6.13ms | |
| elaboration 1.29s | |
| elaboration: tactic compilation 13.4ms | |
| elaboration: tactic execution 1.18s | |
| parsing 21.8ms | |
| type checking 0.905ms | |
| src/data/equiv/basic.lean | |
| cumulative profiling times: | |
| compilation 409ms | |
| decl post-processing 509ms | |
| elaboration 24.6s | |
| elaboration: tactic compilation 2.13s | |
| elaboration: tactic execution 14.5s | |
| parsing 2.99s | |
| type checking 241ms | |
| src/data/equiv/denumerable.lean | |
| cumulative profiling times: | |
| compilation 45.5ms | |
| decl post-processing 53.2ms | |
| elaboration 24s | |
| elaboration: tactic compilation 487ms | |
| elaboration: tactic execution 20.9s | |
| parsing 1.14s | |
| type checking 18.5ms | |
| src/data/equiv/encodable.lean | |
| cumulative profiling times: | |
| compilation 108ms | |
| decl post-processing 221ms | |
| elaboration 15.6s | |
| elaboration: tactic compilation 359ms | |
| elaboration: tactic execution 13s | |
| parsing 782ms | |
| type checking 31.4ms | |
| src/data/equiv/fin.lean | |
| cumulative profiling times: | |
| compilation 36.9ms | |
| decl post-processing 41.5ms | |
| elaboration 3.39s | |
| elaboration: tactic compilation 161ms | |
| elaboration: tactic execution 1.92s | |
| parsing 302ms | |
| type checking 15.5ms | |
| src/data/equiv/functor.lean | |
| cumulative profiling times: | |
| compilation 19.4ms | |
| decl post-processing 14.4ms | |
| elaboration 1.56s | |
| elaboration: tactic compilation 135ms | |
| elaboration: tactic execution 851ms | |
| parsing 400ms | |
| type checking 8.31ms | |
| src/data/equiv/list.lean | |
| cumulative profiling times: | |
| compilation 96.2ms | |
| decl post-processing 82.9ms | |
| elaboration 23.2s | |
| elaboration: tactic compilation 279ms | |
| elaboration: tactic execution 18.7s | |
| parsing 591ms | |
| type checking 18.9ms | |
| src/data/equiv/local_equiv.lean | |
| cumulative profiling times: | |
| compilation 42.1ms | |
| decl post-processing 92.8ms | |
| elaboration 10.7s | |
| elaboration: tactic compilation 754ms | |
| elaboration: tactic execution 7.17s | |
| parsing 1.9s | |
| type checking 50.5ms | |
| src/data/equiv/mul_add.lean | |
| cumulative profiling times: | |
| compilation 67.4ms | |
| decl post-processing 6.47s | |
| elaboration 1.7s | |
| elaboration: tactic compilation 122ms | |
| elaboration: tactic execution 463ms | |
| parsing 214ms | |
| type checking 39.5ms | |
| src/data/equiv/nat.lean | |
| cumulative profiling times: | |
| compilation 8.28ms | |
| decl post-processing 7.67ms | |
| elaboration 2.29s | |
| elaboration: tactic compilation 66.4ms | |
| elaboration: tactic execution 1.86s | |
| parsing 92.1ms | |
| type checking 1.3ms | |
| src/data/equiv/ring.lean | |
| cumulative profiling times: | |
| compilation 90.6ms | |
| decl post-processing 175ms | |
| elaboration 3.38s | |
| elaboration: tactic compilation 168ms | |
| elaboration: tactic execution 1.43s | |
| parsing 295ms | |
| type checking 112ms | |
| src/data/equiv/transfer_instance.lean | |
| cumulative profiling times: | |
| compilation 157ms | |
| decl post-processing 186ms | |
| elaboration 8.73s | |
| elaboration: tactic compilation 180ms | |
| elaboration: tactic execution 7.29s | |
| parsing 259ms | |
| type checking 148ms | |
| src/data/erased.lean | |
| cumulative profiling times: | |
| compilation 41.9ms | |
| decl post-processing 107ms | |
| elaboration 1.16s | |
| elaboration: tactic compilation 58ms | |
| elaboration: tactic execution 879ms | |
| parsing 139ms | |
| type checking 75.5ms | |
| src/data/fin.lean | |
| cumulative profiling times: | |
| compilation 47.4ms | |
| decl post-processing 148ms | |
| elaboration 37.8s | |
| elaboration: tactic compilation 1.67s | |
| elaboration: tactic execution 29.9s | |
| parsing 5.21s | |
| type checking 80.3ms | |
| src/data/fin_enum.lean | |
| cumulative profiling times: | |
| compilation 150ms | |
| decl post-processing 118ms | |
| elaboration 27.8s | |
| elaboration: tactic compilation 508ms | |
| elaboration: tactic execution 22.7s | |
| parsing 1.25s | |
| type checking 50.7ms | |
| src/data/finmap.lean | |
| cumulative profiling times: | |
| compilation 108ms | |
| decl post-processing 241ms | |
| elaboration 57.3s | |
| elaboration: tactic compilation 881ms | |
| elaboration: tactic execution 50.1s | |
| parsing 1.69s | |
| type checking 62.3ms | |
| src/data/finset.lean | |
| cumulative profiling times: | |
| compilation 234ms | |
| decl post-processing 531ms | |
| elaboration 216s | |
| elaboration: tactic compilation 6.63s | |
| elaboration: tactic execution 227s | |
| parsing 14.9s | |
| type checking 315ms | |
| src/data/finsupp.lean | |
| cumulative profiling times: | |
| compilation 58.3ms | |
| decl post-processing 28.7s | |
| elaboration 196s | |
| elaboration: tactic compilation 3.94s | |
| elaboration: tactic execution 78.1s | |
| parsing 8.33s | |
| type checking 247ms | |
| src/data/finsupp/pointwise.lean | |
| cumulative profiling times: | |
| compilation 0.0225ms | |
| decl post-processing 12ms | |
| elaboration 3.84s | |
| elaboration: tactic compilation 75.9ms | |
| elaboration: tactic execution 2.99s | |
| parsing 203ms | |
| type checking 5.24ms | |
| src/data/fintype/basic.lean | |
| cumulative profiling times: | |
| compilation 223ms | |
| decl post-processing 272ms | |
| elaboration 85.9s | |
| elaboration: tactic compilation 1.86s | |
| elaboration: tactic execution 75.5s | |
| parsing 3.56s | |
| type checking 82.7ms | |
| src/data/fintype/card.lean | |
| cumulative profiling times: | |
| compilation 0.0928ms | |
| decl post-processing 33s | |
| elaboration 41.2s | |
| elaboration: tactic compilation 630ms | |
| elaboration: tactic execution 37.6s | |
| parsing 2.14s | |
| type checking 19ms | |
| src/data/fintype/intervals.lean | |
| cumulative profiling times: | |
| compilation 12.4ms | |
| decl post-processing 7.4ms | |
| elaboration 523ms | |
| elaboration: tactic compilation 61.4ms | |
| elaboration: tactic execution 69ms | |
| parsing 88.7ms | |
| type checking 3.54ms | |
| src/data/fp/basic.lean | |
| cumulative profiling times: | |
| compilation 219ms | |
| decl post-processing 48ms | |
| elaboration 3.41s | |
| elaboration: tactic compilation 140ms | |
| elaboration: tactic execution 1.87s | |
| parsing 453ms | |
| type checking 21ms | |
| src/data/hash_map.lean | |
| cumulative profiling times: | |
| compilation 129ms | |
| decl post-processing 129ms | |
| elaboration 32.1s | |
| elaboration: tactic compilation 1.5s | |
| elaboration: tactic execution 26.3s | |
| parsing 5.42s | |
| type checking 76.8ms | |
| src/data/holor.lean | |
| cumulative profiling times: | |
| compilation 79.9ms | |
| decl post-processing 83ms | |
| elaboration 42.4s | |
| elaboration: tactic compilation 765ms | |
| elaboration: tactic execution 39.6s | |
| parsing 1.46s | |
| type checking 42.1ms | |
| src/data/indicator_function.lean | |
| cumulative profiling times: | |
| compilation 0.74ms | |
| decl post-processing 19.5ms | |
| elaboration 19.1s | |
| elaboration: tactic compilation 614ms | |
| elaboration: tactic execution 15.3s | |
| parsing 1.66s | |
| type checking 34.6ms | |
| src/data/int/basic.lean | |
| cumulative profiling times: | |
| compilation 207ms | |
| decl post-processing 914ms | |
| elaboration 82.7s | |
| elaboration: tactic compilation 4.21s | |
| elaboration: tactic execution 58.2s | |
| parsing 8.55s | |
| type checking 92.7ms | |
| src/data/int/gcd.lean | |
| cumulative profiling times: | |
| compilation 4.33ms | |
| decl post-processing 20.4ms | |
| elaboration 14.3s | |
| elaboration: tactic compilation 651ms | |
| elaboration: tactic execution 12.9s | |
| parsing 1.1s | |
| type checking 2.94ms | |
| src/data/int/modeq.lean | |
| cumulative profiling times: | |
| compilation 2.47ms | |
| decl post-processing 4.53ms | |
| elaboration 12.8s | |
| elaboration: tactic compilation 409ms | |
| elaboration: tactic execution 10.7s | |
| parsing 658ms | |
| type checking 3.92ms | |
| src/data/int/parity.lean | |
| cumulative profiling times: | |
| compilation 2.41ms | |
| decl post-processing 5.23ms | |
| elaboration 22.7s | |
| elaboration: tactic compilation 368ms | |
| elaboration: tactic execution 20.9s | |
| parsing 480ms | |
| type checking 2.87ms | |
| src/data/int/sqrt.lean | |
| cumulative profiling times: | |
| compilation 1.16ms | |
| decl post-processing 1.1ms | |
| elaboration 82.5ms | |
| elaboration: tactic compilation 29.2ms | |
| elaboration: tactic execution 0ms | |
| parsing 38.5ms | |
| type checking 0.502ms | |
| src/data/lazy_list2.lean | |
| cumulative profiling times: | |
| compilation 15.3ms | |
| decl post-processing 26.8ms | |
| elaboration 4.89s | |
| elaboration: tactic compilation 157ms | |
| elaboration: tactic execution 3.34s | |
| parsing 421ms | |
| type checking 1.55ms | |
| src/data/list/alist.lean | |
| cumulative profiling times: | |
| compilation 47.8ms | |
| decl post-processing 83.2ms | |
| elaboration 12.7s | |
| elaboration: tactic compilation 373ms | |
| elaboration: tactic execution 10.1s | |
| parsing 766ms | |
| type checking 35.2ms | |
| src/data/list/antidiagonal.lean | |
| cumulative profiling times: | |
| compilation 2.16ms | |
| decl post-processing 2.25ms | |
| elaboration 1.29s | |
| elaboration: tactic compilation 77.7ms | |
| elaboration: tactic execution 1.01s | |
| parsing 127ms | |
| type checking 0.705ms | |
| src/data/list/bag_inter.lean | |
| cumulative profiling times: | |
| compilation 0.0229ms | |
| decl post-processing 4.01ms | |
| elaboration 4.59s | |
| elaboration: tactic compilation 255ms | |
| elaboration: tactic execution 3.45s | |
| parsing 481ms | |
| type checking 2.59ms | |
| src/data/list/basic.lean | |
| cumulative profiling times: | |
| compilation 49.7ms | |
| decl post-processing 6.26s | |
| elaboration 118s | |
| elaboration: tactic compilation 9.73s | |
| elaboration: tactic execution 72.3s | |
| parsing 20.2s | |
| type checking 256ms | |
| src/data/list/chain.lean | |
| cumulative profiling times: | |
| compilation 0.0968ms | |
| decl post-processing 1.29ms | |
| elaboration 4.07s | |
| elaboration: tactic compilation 438ms | |
| elaboration: tactic execution 2.21s | |
| parsing 1.05s | |
| type checking 10.4ms | |
| src/data/list/default.lean | |
| src/data/list/defs.lean | |
| cumulative profiling times: | |
| compilation 103ms | |
| decl post-processing 162ms | |
| elaboration 1.27s | |
| elaboration: tactic compilation 66.3ms | |
| elaboration: tactic execution 23ms | |
| parsing 136ms | |
| type checking 12.6ms | |
| src/data/list/erase_dup.lean | |
| cumulative profiling times: | |
| compilation 0.0333ms | |
| decl post-processing 2.11ms | |
| elaboration 490ms | |
| elaboration: tactic compilation 51.1ms | |
| elaboration: tactic execution 135ms | |
| parsing 164ms | |
| type checking 2.85ms | |
| src/data/list/forall2.lean | |
| cumulative profiling times: | |
| compilation 0.0893ms | |
| decl post-processing 311ms | |
| elaboration 4.74s | |
| elaboration: tactic compilation 398ms | |
| elaboration: tactic execution 1.85s | |
| parsing 806ms | |
| type checking 10.2ms | |
| src/data/list/func.lean | |
| cumulative profiling times: | |
| compilation 8.46ms | |
| decl post-processing 30.7ms | |
| elaboration 7.51s | |
| elaboration: tactic compilation 808ms | |
| elaboration: tactic execution 4.02s | |
| parsing 1.74s | |
| type checking 7.33ms | |
| src/data/list/intervals.lean | |
| cumulative profiling times: | |
| compilation 0.862ms | |
| decl post-processing 3.51ms | |
| elaboration 9.53s | |
| elaboration: tactic compilation 499ms | |
| elaboration: tactic execution 7.55s | |
| parsing 869ms | |
| type checking 5.01ms | |
| src/data/list/min_max.lean | |
| cumulative profiling times: | |
| compilation 12ms | |
| decl post-processing 15.2ms | |
| elaboration 18.6s | |
| elaboration: tactic compilation 478ms | |
| elaboration: tactic execution 15.8s | |
| parsing 1.54s | |
| type checking 24.7ms | |
| src/data/list/nodup.lean | |
| cumulative profiling times: | |
| compilation 0.128ms | |
| decl post-processing 3.17ms | |
| elaboration 3.38s | |
| elaboration: tactic compilation 425ms | |
| elaboration: tactic execution 1.72s | |
| parsing 724ms | |
| type checking 9.53ms | |
| src/data/list/of_fn.lean | |
| cumulative profiling times: | |
| compilation 0.039ms | |
| decl post-processing 2.04ms | |
| elaboration 2.56s | |
| elaboration: tactic compilation 202ms | |
| elaboration: tactic execution 2.46s | |
| parsing 359ms | |
| type checking 3.29ms | |
| src/data/list/pairwise.lean | |
| cumulative profiling times: | |
| compilation 0.118ms | |
| decl post-processing 4.23ms | |
| elaboration 4.57s | |
| elaboration: tactic compilation 786ms | |
| elaboration: tactic execution 1.75s | |
| parsing 1.86s | |
| type checking 16.9ms | |
| src/data/list/perm.lean | |
| cumulative profiling times: | |
| compilation 2.75ms | |
| decl post-processing 988ms | |
| elaboration 31.7s | |
| elaboration: tactic compilation 2.32s | |
| elaboration: tactic execution 23.6s | |
| parsing 5.97s | |
| type checking 32.5ms | |
| src/data/list/range.lean | |
| cumulative profiling times: | |
| compilation 1.76ms | |
| decl post-processing 916ms | |
| elaboration 5.29s | |
| elaboration: tactic compilation 615ms | |
| elaboration: tactic execution 5.46s | |
| parsing 1.12s | |
| type checking 11.4ms | |
| src/data/list/rotate.lean | |
| cumulative profiling times: | |
| compilation 0.0481ms | |
| decl post-processing 2.58ms | |
| elaboration 10.7s | |
| elaboration: tactic compilation 465ms | |
| elaboration: tactic execution 8.42s | |
| parsing 738ms | |
| type checking 2.75ms | |
| src/data/list/sections.lean | |
| cumulative profiling times: | |
| compilation 0.0067ms | |
| decl post-processing 0.0173ms | |
| elaboration 529ms | |
| elaboration: tactic compilation 82.5ms | |
| elaboration: tactic execution 270ms | |
| parsing 329ms | |
| type checking 0.847ms | |
| src/data/list/sigma.lean | |
| cumulative profiling times: | |
| compilation 24.8ms | |
| decl post-processing 62.4ms | |
| elaboration 56.1s | |
| elaboration: tactic compilation 1.84s | |
| elaboration: tactic execution 48.1s | |
| parsing 4.99s | |
| type checking 45.4ms | |
| src/data/list/sort.lean | |
| cumulative profiling times: | |
| compilation 4.93ms | |
| decl post-processing 31.8ms | |
| elaboration 17.9s | |
| elaboration: tactic compilation 935ms | |
| elaboration: tactic execution 13.1s | |
| parsing 1.36s | |
| type checking 5.88ms | |
| src/data/list/tfae.lean | |
| cumulative profiling times: | |
| compilation 0.14ms | |
| decl post-processing 2.08ms | |
| elaboration 1.97s | |
| elaboration: tactic compilation 88.2ms | |
| elaboration: tactic execution 1.64s | |
| parsing 160ms | |
| type checking 0.965ms | |
| src/data/list/zip.lean | |
| cumulative profiling times: | |
| compilation 0.0747ms | |
| decl post-processing 3.78ms | |
| elaboration 3.58s | |
| elaboration: tactic compilation 396ms | |
| elaboration: tactic execution 1.73s | |
| parsing 600ms | |
| type checking 8.26ms | |
| src/data/matrix/basic.lean | |
| cumulative profiling times: | |
| compilation 262ms | |
| decl post-processing 546ms | |
| elaboration 144s | |
| elaboration: tactic compilation 1.85s | |
| elaboration: tactic execution 128s | |
| parsing 3.47s | |
| type checking 211ms | |
| src/data/matrix/notation.lean | |
| cumulative profiling times: | |
| compilation 4.25ms | |
| decl post-processing 46.1ms | |
| elaboration 90.8s | |
| elaboration: tactic compilation 693ms | |
| elaboration: tactic execution 84.4s | |
| parsing 1.29s | |
| type checking 35.8ms | |
| src/data/matrix/pequiv.lean | |
| cumulative profiling times: | |
| compilation 4.84ms | |
| decl post-processing 13.9ms | |
| elaboration 30.9s | |
| elaboration: tactic compilation 289ms | |
| elaboration: tactic execution 28.4s | |
| parsing 869ms | |
| type checking 18ms | |
| src/data/mllist.lean | |
| cumulative profiling times: | |
| compilation 50ms | |
| decl post-processing 0.106ms | |
| elaboration 522ms | |
| parsing 16.9ms | |
| type checking 6.43ms | |
| src/data/monoid_algebra.lean | |
| cumulative profiling times: | |
| compilation 1.33ms | |
| decl post-processing 485ms | |
| elaboration 106s | |
| elaboration: tactic compilation 1.4s | |
| elaboration: tactic execution 72.6s | |
| parsing 3s | |
| type checking 381ms | |
| src/data/multiset.lean | |
| cumulative profiling times: | |
| compilation 360ms | |
| decl post-processing 11s | |
| elaboration 382s | |
| elaboration: tactic compilation 6.23s | |
| elaboration: tactic execution 349s | |
| parsing 13.5s | |
| type checking 463ms | |
| src/data/mv_polynomial.lean | |
| cumulative profiling times: | |
| compilation 34.7ms | |
| decl post-processing 530ms | |
| elaboration 300s | |
| elaboration: tactic compilation 3.04s | |
| elaboration: tactic execution 226s | |
| parsing 7.06s | |
| type checking 380ms | |
| src/data/nat/basic.lean | |
| cumulative profiling times: | |
| compilation 39.2ms | |
| decl post-processing 1.09s | |
| elaboration 47.7s | |
| elaboration: tactic compilation 4.24s | |
| elaboration: tactic execution 29.2s | |
| parsing 8.34s | |
| type checking 66.2ms | |
| src/data/nat/cast.lean | |
| cumulative profiling times: | |
| compilation 7.71ms | |
| decl post-processing 367ms | |
| elaboration 5.5s | |
| elaboration: tactic compilation 201ms | |
| elaboration: tactic execution 3.78s | |
| parsing 358ms | |
| type checking 33.9ms | |
| src/data/nat/choose.lean | |
| cumulative profiling times: | |
| compilation 0.0146ms | |
| decl post-processing 0.02ms | |
| elaboration 3.83s | |
| elaboration: tactic compilation 208ms | |
| elaboration: tactic execution 5.69s | |
| parsing 631ms | |
| type checking 1.93ms | |
| src/data/nat/dist.lean | |
| cumulative profiling times: | |
| compilation 0.835ms | |
| decl post-processing 0.888ms | |
| elaboration 3.54s | |
| elaboration: tactic compilation 305ms | |
| elaboration: tactic execution 2.54s | |
| parsing 378ms | |
| type checking 1.57ms | |
| src/data/nat/enat.lean | |
| cumulative profiling times: | |
| compilation 44.6ms | |
| decl post-processing 157ms | |
| elaboration 12.8s | |
| elaboration: tactic compilation 546ms | |
| elaboration: tactic execution 10s | |
| parsing 1.19s | |
| type checking 34.8ms | |
| src/data/nat/fib.lean | |
| cumulative profiling times: | |
| compilation 2.49ms | |
| decl post-processing 3.15ms | |
| elaboration 3.27s | |
| elaboration: tactic compilation 159ms | |
| elaboration: tactic execution 2.67s | |
| parsing 702ms | |
| type checking 1.16ms | |
| src/data/nat/gcd.lean | |
| cumulative profiling times: | |
| compilation 23.4ms | |
| decl post-processing 20.9ms | |
| elaboration 5.97s | |
| elaboration: tactic compilation 732ms | |
| elaboration: tactic execution 3.49s | |
| parsing 1.44s | |
| type checking 16.1ms | |
| src/data/nat/modeq.lean | |
| cumulative profiling times: | |
| compilation 5.16ms | |
| decl post-processing 22.7ms | |
| elaboration 16.6s | |
| elaboration: tactic compilation 893ms | |
| elaboration: tactic execution 12.9s | |
| parsing 1.85s | |
| type checking 6.02ms | |
| src/data/nat/multiplicity.lean | |
| cumulative profiling times: | |
| compilation 0.0361ms | |
| decl post-processing 0.0408ms | |
| elaboration 21s | |
| elaboration: tactic compilation 519ms | |
| elaboration: tactic execution 19.8s | |
| parsing 1.02s | |
| type checking 4.77ms | |
| src/data/nat/pairing.lean | |
| cumulative profiling times: | |
| compilation 6.07ms | |
| decl post-processing 3.38ms | |
| elaboration 7.29s | |
| elaboration: tactic compilation 262ms | |
| elaboration: tactic execution 6.12s | |
| parsing 939ms | |
| type checking 1.21ms | |
| src/data/nat/parity.lean | |
| cumulative profiling times: | |
| compilation 2.15ms | |
| decl post-processing 4.25ms | |
| elaboration 13.9s | |
| elaboration: tactic compilation 389ms | |
| elaboration: tactic execution 12.1s | |
| parsing 667ms | |
| type checking 2.34ms | |
| src/data/nat/prime.lean | |
| cumulative profiling times: | |
| compilation 30.5ms | |
| decl post-processing 26.5ms | |
| elaboration 17.2s | |
| elaboration: tactic compilation 1.21s | |
| elaboration: tactic execution 11.3s | |
| parsing 1.99s | |
| type checking 12.5ms | |
| src/data/nat/sqrt.lean | |
| cumulative profiling times: | |
| compilation 2.32ms | |
| decl post-processing 2.96ms | |
| elaboration 6.85s | |
| elaboration: tactic compilation 524ms | |
| elaboration: tactic execution 4.97s | |
| parsing 1.25s | |
| type checking 7.11ms | |
| src/data/nat/totient.lean | |
| cumulative profiling times: | |
| compilation 1.39ms | |
| decl post-processing 1.25ms | |
| elaboration 6.03s | |
| elaboration: tactic compilation 203ms | |
| elaboration: tactic execution 4.6s | |
| parsing 323ms | |
| type checking 0.633ms | |
| src/data/num/basic.lean | |
| cumulative profiling times: | |
| compilation 45.6ms | |
| decl post-processing 114ms | |
| elaboration 982ms | |
| elaboration: tactic compilation 62.5ms | |
| elaboration: tactic execution 188ms | |
| parsing 87.3ms | |
| type checking 3.26ms | |
| src/data/num/bitwise.lean | |
| cumulative profiling times: | |
| compilation 23.6ms | |
| decl post-processing 60.4ms | |
| elaboration 483ms | |
| elaboration: tactic compilation 35.2ms | |
| elaboration: tactic execution 0ms | |
| parsing 48.1ms | |
| type checking 1.74ms | |
| src/data/num/lemmas.lean | |
| cumulative profiling times: | |
| compilation 346ms | |
| decl post-processing 1.49s | |
| elaboration 76.6s | |
| elaboration: tactic compilation 4.8s | |
| elaboration: tactic execution 54.4s | |
| parsing 8.65s | |
| type checking 97.4ms | |
| src/data/opposite.lean | |
| cumulative profiling times: | |
| compilation 41.9ms | |
| decl post-processing 5.09ms | |
| elaboration 100ms | |
| elaboration: tactic compilation 23.3ms | |
| elaboration: tactic execution 0ms | |
| parsing 31ms | |
| type checking 3.64ms | |
| src/data/option/basic.lean | |
| cumulative profiling times: | |
| compilation 0.677ms | |
| decl post-processing 27.7ms | |
| elaboration 3.89s | |
| elaboration: tactic compilation 348ms | |
| elaboration: tactic execution 2.43s | |
| parsing 603ms | |
| type checking 12ms | |
| src/data/option/defs.lean | |
| cumulative profiling times: | |
| compilation 13.2ms | |
| decl post-processing 70.9ms | |
| elaboration 1.08s | |
| elaboration: tactic compilation 109ms | |
| elaboration: tactic execution 524ms | |
| parsing 218ms | |
| type checking 19.7ms | |
| src/data/padics/default.lean | |
| src/data/padics/hensel.lean | |
| cumulative profiling times: | |
| compilation 2.32ms | |
| decl post-processing 160ms | |
| elaboration 68s | |
| elaboration: tactic compilation 1.14s | |
| elaboration: tactic execution 56.2s | |
| parsing 2.29s | |
| type checking 133ms | |
| src/data/padics/padic_integers.lean | |
| cumulative profiling times: | |
| compilation 9.76ms | |
| decl post-processing 474ms | |
| elaboration 114s | |
| elaboration: tactic compilation 616ms | |
| elaboration: tactic execution 110s | |
| parsing 1.44s | |
| type checking 76.3ms | |
| src/data/padics/padic_norm.lean | |
| cumulative profiling times: | |
| compilation 18.9ms | |
| decl post-processing 17.9ms | |
| elaboration 57.5s | |
| elaboration: tactic compilation 1.06s | |
| elaboration: tactic execution 56.3s | |
| parsing 2.15s | |
| type checking 24.1ms | |
| src/data/padics/padic_numbers.lean | |
| cumulative profiling times: | |
| compilation 87.4ms | |
| decl post-processing 593ms | |
| elaboration 211s | |
| elaboration: tactic compilation 2.01s | |
| elaboration: tactic execution 189s | |
| parsing 5.3s | |
| type checking 344ms | |
| src/data/pequiv.lean | |
| cumulative profiling times: | |
| compilation 72.5ms | |
| decl post-processing 98.8ms | |
| elaboration 46.5s | |
| elaboration: tactic compilation 598ms | |
| elaboration: tactic execution 41.9s | |
| parsing 1.83s | |
| type checking 82.7ms | |
| src/data/pfun.lean | |
| cumulative profiling times: | |
| compilation 113ms | |
| decl post-processing 293ms | |
| elaboration 27.5s | |
| elaboration: tactic compilation 813ms | |
| elaboration: tactic execution 23.4s | |
| parsing 1.62s | |
| type checking 179ms | |
| src/data/pnat/basic.lean | |
| cumulative profiling times: | |
| compilation 52.8ms | |
| decl post-processing 115ms | |
| elaboration 5.07s | |
| elaboration: tactic compilation 458ms | |
| elaboration: tactic execution 2.65s | |
| parsing 1.18s | |
| type checking 27.7ms | |
| src/data/pnat/factors.lean | |
| cumulative profiling times: | |
| compilation 27.9ms | |
| decl post-processing 39.9ms | |
| elaboration 11.9s | |
| elaboration: tactic compilation 843ms | |
| elaboration: tactic execution 8.58s | |
| parsing 2.56s | |
| type checking 30.3ms | |
| src/data/pnat/intervals.lean | |
| cumulative profiling times: | |
| compilation 4.82ms | |
| decl post-processing 4.9ms | |
| elaboration 4.19s | |
| elaboration: tactic compilation 39.5ms | |
| elaboration: tactic execution 3.83s | |
| parsing 86.1ms | |
| type checking 3.05ms | |
| src/data/pnat/xgcd.lean | |
| cumulative profiling times: | |
| compilation 34.5ms | |
| decl post-processing 38.5ms | |
| elaboration 13.3s | |
| elaboration: tactic compilation 754ms | |
| elaboration: tactic execution 10.1s | |
| parsing 2.75s | |
| type checking 33.2ms | |
| src/data/polynomial.lean | |
| cumulative profiling times: | |
| compilation 158ms | |
| decl post-processing 1.19s | |
| elaboration 472s | |
| elaboration: tactic compilation 8.2s | |
| elaboration: tactic execution 384s | |
| parsing 16s | |
| type checking 1.13s | |
| src/data/prod.lean | |
| cumulative profiling times: | |
| compilation 16ms | |
| decl post-processing 18.6ms | |
| elaboration 1.18s | |
| elaboration: tactic compilation 96.8ms | |
| elaboration: tactic execution 752ms | |
| parsing 102ms | |
| type checking 6.62ms | |
| src/data/quot.lean | |
| cumulative profiling times: | |
| compilation 59.4ms | |
| decl post-processing 120ms | |
| elaboration 525ms | |
| elaboration: tactic compilation 42.8ms | |
| elaboration: tactic execution 105ms | |
| parsing 52ms | |
| type checking 68.4ms | |
| src/data/rat/basic.lean | |
| cumulative profiling times: | |
| compilation 60.2ms | |
| decl post-processing 165ms | |
| elaboration 59.9s | |
| elaboration: tactic compilation 1.99s | |
| elaboration: tactic execution 52s | |
| parsing 5.23s | |
| type checking 30.4ms | |
| src/data/rat/cast.lean | |
| cumulative profiling times: | |
| compilation 13.2ms | |
| decl post-processing 921ms | |
| elaboration 20.8s | |
| elaboration: tactic compilation 710ms | |
| elaboration: tactic execution 17.6s | |
| parsing 1.99s | |
| type checking 44.6ms | |
| src/data/rat/default.lean | |
| src/data/rat/denumerable.lean | |
| cumulative profiling times: | |
| compilation 17ms | |
| decl post-processing 9.49ms | |
| elaboration 366ms | |
| elaboration: tactic compilation 22.6ms | |
| elaboration: tactic execution 74ms | |
| parsing 159ms | |
| type checking 7.39ms | |
| src/data/rat/floor.lean | |
| cumulative profiling times: | |
| compilation 1.68ms | |
| decl post-processing 5.58ms | |
| elaboration 1.35s | |
| elaboration: tactic compilation 36.3ms | |
| elaboration: tactic execution 1.16s | |
| parsing 122ms | |
| type checking 5.94ms | |
| src/data/rat/meta_defs.lean | |
| cumulative profiling times: | |
| compilation 236ms | |
| decl post-processing 0.221ms | |
| elaboration 656ms | |
| elaboration: tactic compilation 48.5ms | |
| elaboration: tactic execution 0ms | |
| parsing 12.6ms | |
| type checking 17.7ms | |
| src/data/rat/order.lean | |
| cumulative profiling times: | |
| compilation 45.4ms | |
| decl post-processing 56.1ms | |
| elaboration 14.1s | |
| elaboration: tactic compilation 922ms | |
| elaboration: tactic execution 10.9s | |
| parsing 1.72s | |
| type checking 23.2ms | |
| src/data/real/basic.lean | |
| cumulative profiling times: | |
| compilation 52.8ms | |
| decl post-processing 245ms | |
| elaboration 63.2s | |
| elaboration: tactic compilation 1.95s | |
| elaboration: tactic execution 56.4s | |
| parsing 4.31s | |
| type checking 273ms | |
| src/data/real/cardinality.lean | |
| cumulative profiling times: | |
| compilation 4.63ms | |
| decl post-processing 4.98ms | |
| elaboration 45s | |
| elaboration: tactic compilation 454ms | |
| elaboration: tactic execution 41.9s | |
| parsing 1.7s | |
| type checking 3.04ms | |
| src/data/real/cau_seq.lean | |
| cumulative profiling times: | |
| compilation 133ms | |
| decl post-processing 206ms | |
| elaboration 52.5s | |
| elaboration: tactic compilation 1.15s | |
| elaboration: tactic execution 42.9s | |
| parsing 3.57s | |
| type checking 145ms | |
| src/data/real/cau_seq_completion.lean | |
| cumulative profiling times: | |
| compilation 85ms | |
| decl post-processing 135ms | |
| elaboration 26.6s | |
| elaboration: tactic compilation 413ms | |
| elaboration: tactic execution 22.1s | |
| parsing 862ms | |
| type checking 194ms | |
| src/data/real/ennreal.lean | |
| cumulative profiling times: | |
| compilation 6.19ms | |
| decl post-processing 1.52s | |
| elaboration 187s | |
| elaboration: tactic compilation 3.17s | |
| elaboration: tactic execution 168s | |
| parsing 7.63s | |
| type checking 129ms | |
| src/data/real/ereal.lean | |
| cumulative profiling times: | |
| compilation 2.07ms | |
| decl post-processing 347ms | |
| elaboration 9.62s | |
| elaboration: tactic compilation 180ms | |
| elaboration: tactic execution 8.66s | |
| parsing 216ms | |
| type checking 1.76ms | |
| src/data/real/hyperreal.lean | |
| cumulative profiling times: | |
| compilation 3.48ms | |
| decl post-processing 363ms | |
| elaboration 61.1s | |
| elaboration: tactic compilation 1.8s | |
| elaboration: tactic execution 54.4s | |
| parsing 3.01s | |
| type checking 43.1ms | |
| src/data/real/irrational.lean | |
| cumulative profiling times: | |
| compilation 13.3ms | |
| decl post-processing 5.36ms | |
| elaboration 9.43s | |
| elaboration: tactic compilation 377ms | |
| elaboration: tactic execution 7.41s | |
| parsing 866ms | |
| type checking 17.2ms | |
| src/data/real/nnreal.lean | |
| cumulative profiling times: | |
| compilation 99.5ms | |
| decl post-processing 889ms | |
| elaboration 60.7s | |
| elaboration: tactic compilation 1.31s | |
| elaboration: tactic execution 51.1s | |
| parsing 2.48s | |
| type checking 144ms | |
| src/data/real/pi.lean | |
| cumulative profiling times: | |
| compilation 68.4ms | |
| decl post-processing 5.36ms | |
| elaboration 80.9s | |
| elaboration: tactic compilation 1.02s | |
| elaboration: tactic execution 72.6s | |
| parsing 2.6s | |
| type checking 16.4ms | |
| src/data/rel.lean | |
| cumulative profiling times: | |
| compilation 3.08ms | |
| decl post-processing 45.6ms | |
| elaboration 12s | |
| elaboration: tactic compilation 384ms | |
| elaboration: tactic execution 9.87s | |
| parsing 679ms | |
| type checking 12.1ms | |
| src/data/semiquot.lean | |
| cumulative profiling times: | |
| compilation 76.8ms | |
| decl post-processing 294ms | |
| elaboration 6.29s | |
| elaboration: tactic compilation 166ms | |
| elaboration: tactic execution 4.93s | |
| parsing 251ms | |
| type checking 219ms | |
| src/data/seq/computation.lean | |
| cumulative profiling times: | |
| compilation 112ms | |
| decl post-processing 234ms | |
| elaboration 13.8s | |
| elaboration: tactic compilation 1.73s | |
| elaboration: tactic execution 8.43s | |
| parsing 3.93s | |
| type checking 105ms | |
| src/data/seq/parallel.lean | |
| cumulative profiling times: | |
| compilation 25.6ms | |
| decl post-processing 63.2ms | |
| elaboration 12.9s | |
| elaboration: tactic compilation 711ms | |
| elaboration: tactic execution 12s | |
| parsing 3.82s | |
| type checking 9.78ms | |
| src/data/seq/seq.lean | |
| cumulative profiling times: | |
| compilation 106ms | |
| decl post-processing 222ms | |
| elaboration 46.3s | |
| elaboration: tactic compilation 1.63s | |
| elaboration: tactic execution 45.2s | |
| parsing 4.39s | |
| type checking 76.6ms | |
| src/data/seq/wseq.lean | |
| cumulative profiling times: | |
| compilation 235ms | |
| decl post-processing 144ms | |
| elaboration 85.6s | |
| elaboration: tactic compilation 3.1s | |
| elaboration: tactic execution 83s | |
| parsing 6.98s | |
| type checking 40.5ms | |
| src/data/set/basic.lean | |
| cumulative profiling times: | |
| compilation 20.2ms | |
| decl post-processing 98.1ms | |
| elaboration 92.9s | |
| elaboration: tactic compilation 2.75s | |
| elaboration: tactic execution 77.1s | |
| parsing 5.36s | |
| type checking 114ms | |
| src/data/set/countable.lean | |
| cumulative profiling times: | |
| compilation 0.239ms | |
| decl post-processing 9.19ms | |
| elaboration 21s | |
| elaboration: tactic compilation 420ms | |
| elaboration: tactic execution 24.5s | |
| parsing 1.1s | |
| type checking 4.94ms | |
| src/data/set/default.lean | |
| src/data/set/disjointed.lean | |
| cumulative profiling times: | |
| compilation 0.497ms | |
| decl post-processing 2.41ms | |
| elaboration 9.08s | |
| elaboration: tactic compilation 189ms | |
| elaboration: tactic execution 7.9s | |
| parsing 467ms | |
| type checking 2.69ms | |
| src/data/set/enumerate.lean | |
| cumulative profiling times: | |
| compilation 1.08ms | |
| decl post-processing 5.32ms | |
| elaboration 7.13s | |
| elaboration: tactic compilation 190ms | |
| elaboration: tactic execution 6.09s | |
| parsing 726ms | |
| type checking 1.07ms | |
| src/data/set/finite.lean | |
| cumulative profiling times: | |
| compilation 78.9ms | |
| decl post-processing 758ms | |
| elaboration 41.5s | |
| elaboration: tactic compilation 911ms | |
| elaboration: tactic execution 44.4s | |
| parsing 2.01s | |
| type checking 48.1ms | |
| src/data/set/function.lean | |
| cumulative profiling times: | |
| compilation 6.87ms | |
| decl post-processing 31.9ms | |
| elaboration 5s | |
| elaboration: tactic compilation 368ms | |
| elaboration: tactic execution 3.4s | |
| parsing 867ms | |
| type checking 29.7ms | |
| src/data/set/intervals/basic.lean | |
| cumulative profiling times: | |
| compilation 2.07ms | |
| decl post-processing 54.8ms | |
| elaboration 30s | |
| elaboration: tactic compilation 836ms | |
| elaboration: tactic execution 24.4s | |
| parsing 1.55s | |
| type checking 49ms | |
| src/data/set/intervals/default.lean | |
| src/data/set/intervals/disjoint.lean | |
| cumulative profiling times: | |
| compilation 0.0063ms | |
| decl post-processing 0.0139ms | |
| elaboration 196ms | |
| elaboration: tactic compilation 23.6ms | |
| elaboration: tactic execution 117ms | |
| parsing 37.9ms | |
| type checking 0.764ms | |
| src/data/set/intervals/unordered_interval.lean | |
| cumulative profiling times: | |
| compilation 0.349ms | |
| decl post-processing 4.43ms | |
| elaboration 2.51s | |
| elaboration: tactic compilation 210ms | |
| elaboration: tactic execution 1.61s | |
| parsing 288ms | |
| type checking 6.99ms | |
| src/data/set/lattice.lean | |
| cumulative profiling times: | |
| compilation 84.4ms | |
| decl post-processing 449ms | |
| elaboration 48.8s | |
| elaboration: tactic compilation 1.43s | |
| elaboration: tactic execution 40.1s | |
| parsing 2.55s | |
| type checking 420ms | |
| src/data/setoid.lean | |
| cumulative profiling times: | |
| compilation 94.8ms | |
| decl post-processing 147ms | |
| elaboration 3.24s | |
| elaboration: tactic compilation 344ms | |
| elaboration: tactic execution 929ms | |
| parsing 620ms | |
| type checking 81.2ms | |
| src/data/sigma/basic.lean | |
| cumulative profiling times: | |
| compilation 9.17ms | |
| decl post-processing 18.5ms | |
| elaboration 440ms | |
| elaboration: tactic compilation 28.6ms | |
| elaboration: tactic execution 147ms | |
| parsing 96.5ms | |
| type checking 2.69ms | |
| src/data/sigma/default.lean | |
| src/data/stream/basic.lean | |
| cumulative profiling times: | |
| compilation 0.815ms | |
| decl post-processing 0.851ms | |
| elaboration 0.414ms | |
| parsing 0.132ms | |
| type checking 0.0579ms | |
| src/data/string/basic.lean | |
| cumulative profiling times: | |
| compilation 13.5ms | |
| decl post-processing 9.26ms | |
| elaboration 3.18s | |
| elaboration: tactic compilation 129ms | |
| elaboration: tactic execution 2.9s | |
| parsing 175ms | |
| type checking 2.37ms | |
| src/data/string/defs.lean | |
| cumulative profiling times: | |
| compilation 9.22ms | |
| decl post-processing 4.48ms | |
| elaboration 38.7ms | |
| parsing 0.696ms | |
| type checking 0.716ms | |
| src/data/subtype.lean | |
| cumulative profiling times: | |
| compilation 6.54ms | |
| decl post-processing 12.3ms | |
| elaboration 162ms | |
| elaboration: tactic compilation 43.9ms | |
| elaboration: tactic execution 5ms | |
| parsing 13.2ms | |
| type checking 7.12ms | |
| src/data/sum.lean | |
| cumulative profiling times: | |
| compilation 3.38ms | |
| decl post-processing 11ms | |
| elaboration 350ms | |
| elaboration: tactic compilation 105ms | |
| elaboration: tactic execution 1ms | |
| parsing 141ms | |
| type checking 3.69ms | |
| src/data/support.lean | |
| cumulative profiling times: | |
| compilation 0.383ms | |
| decl post-processing 3.81ms | |
| elaboration 4.5s | |
| elaboration: tactic compilation 112ms | |
| elaboration: tactic execution 3.72s | |
| parsing 240ms | |
| type checking 6.26ms | |
| src/data/tree.lean | |
| cumulative profiling times: | |
| compilation 4.49ms | |
| decl post-processing 13.6ms | |
| elaboration 106ms | |
| parsing 2.5ms | |
| type checking 0.375ms | |
| src/data/ulift.lean | |
| cumulative profiling times: | |
| compilation 0.0067ms | |
| decl post-processing 0.568ms | |
| elaboration 5.78ms | |
| parsing 0.758ms | |
| type checking 0.416ms | |
| src/data/vector2.lean | |
| cumulative profiling times: | |
| compilation 22.3ms | |
| decl post-processing 83.9ms | |
| elaboration 20.1s | |
| elaboration: tactic compilation 609ms | |
| elaboration: tactic execution 15.9s | |
| parsing 1.56s | |
| type checking 26.3ms | |
| src/data/zmod/basic.lean | |
| cumulative profiling times: | |
| compilation 52.1ms | |
| decl post-processing 191ms | |
| elaboration 34.2s | |
| elaboration: tactic compilation 1.74s | |
| elaboration: tactic execution 29.2s | |
| parsing 3.9s | |
| type checking 128ms | |
| src/data/zsqrtd/basic.lean | |
| cumulative profiling times: | |
| compilation 109ms | |
| decl post-processing 138ms | |
| elaboration 59s | |
| elaboration: tactic compilation 1.64s | |
| elaboration: tactic execution 54s | |
| parsing 2.93s | |
| type checking 55.6ms | |
| src/data/zsqrtd/gaussian_int.lean | |
| cumulative profiling times: | |
| compilation 24.6ms | |
| decl post-processing 87.5ms | |
| elaboration 98.1s | |
| elaboration: tactic compilation 918ms | |
| elaboration: tactic execution 93s | |
| parsing 2.16s | |
| type checking 129ms | |
| src/deprecated/group.lean | |
| cumulative profiling times: | |
| compilation 4.15ms | |
| decl post-processing 3.76s | |
| elaboration 1.02s | |
| elaboration: tactic compilation 87.5ms | |
| elaboration: tactic execution 307ms | |
| parsing 137ms | |
| type checking 17.3ms | |
| src/field_theory/finite.lean | |
| cumulative profiling times: | |
| compilation 16.2ms | |
| decl post-processing 22.7ms | |
| elaboration 34.7s | |
| elaboration: tactic compilation 485ms | |
| elaboration: tactic execution 44.4s | |
| parsing 1.25s | |
| type checking 26.8ms | |
| src/field_theory/minimal_polynomial.lean | |
| cumulative profiling times: | |
| compilation 0.0578ms | |
| decl post-processing 20.3ms | |
| elaboration 43.8s | |
| elaboration: tactic compilation 315ms | |
| elaboration: tactic execution 47.6s | |
| parsing 1.3s | |
| type checking 464ms | |
| src/field_theory/mv_polynomial.lean | |
| cumulative profiling times: | |
| compilation 5.66ms | |
| decl post-processing 289ms | |
| elaboration 17.4s | |
| elaboration: tactic compilation 463ms | |
| elaboration: tactic execution 11.8s | |
| parsing 889ms | |
| type checking 260ms | |
| src/field_theory/perfect_closure.lean | |
| cumulative profiling times: | |
| compilation 155ms | |
| decl post-processing 281ms | |
| elaboration 9.81s | |
| elaboration: tactic compilation 575ms | |
| elaboration: tactic execution 3.96s | |
| parsing 1.56s | |
| type checking 320ms | |
| src/field_theory/splitting_field.lean | |
| cumulative profiling times: | |
| compilation 0.381ms | |
| decl post-processing 24.8ms | |
| elaboration 42.9s | |
| elaboration: tactic compilation 464ms | |
| elaboration: tactic execution 19.8s | |
| parsing 938ms | |
| type checking 109ms | |
| src/field_theory/subfield.lean | |
| cumulative profiling times: | |
| compilation 18.2ms | |
| decl post-processing 184ms | |
| elaboration 3.66s | |
| elaboration: tactic compilation 127ms | |
| elaboration: tactic execution 1.8s | |
| parsing 182ms | |
| type checking 119ms | |
| src/geometry/manifold/basic_smooth_bundle.lean | |
| cumulative profiling times: | |
| compilation 78.3ms | |
| decl post-processing 890ms | |
| elaboration 136s | |
| elaboration: tactic compilation 640ms | |
| elaboration: tactic execution 124s | |
| parsing 3.37s | |
| type checking 487ms | |
| src/geometry/manifold/manifold.lean | |
| cumulative profiling times: | |
| compilation 56.4ms | |
| decl post-processing 82.3ms | |
| elaboration 21.8s | |
| elaboration: tactic compilation 600ms | |
| elaboration: tactic execution 15.5s | |
| parsing 2.44s | |
| type checking 42.6ms | |
| src/geometry/manifold/mfderiv.lean | |
| cumulative profiling times: | |
| compilation 14.3ms | |
| decl post-processing 432ms | |
| elaboration 234s | |
| elaboration: tactic compilation 1.53s | |
| elaboration: tactic execution 216s | |
| parsing 6.15s | |
| type checking 1.47s | |
| src/geometry/manifold/real_instances.lean | |
| cumulative profiling times: | |
| compilation 10.1ms | |
| decl post-processing 302ms | |
| elaboration 57.3s | |
| elaboration: tactic compilation 734ms | |
| elaboration: tactic execution 52.4s | |
| parsing 2.46s | |
| type checking 233ms | |
| src/geometry/manifold/smooth_manifold_with_corners.lean | |
| cumulative profiling times: | |
| compilation 22.8ms | |
| decl post-processing 90ms | |
| elaboration 60.3s | |
| elaboration: tactic compilation 610ms | |
| elaboration: tactic execution 52.8s | |
| parsing 1.62s | |
| type checking 71.9ms | |
| src/group_theory/abelianization.lean | |
| cumulative profiling times: | |
| compilation 23.3ms | |
| decl post-processing 19.4ms | |
| elaboration 3.54s | |
| elaboration: tactic compilation 22.4ms | |
| elaboration: tactic execution 3.02s | |
| parsing 46.4ms | |
| type checking 7.84ms | |
| src/group_theory/bundled_subgroup.lean | |
| cumulative profiling times: | |
| compilation 132ms | |
| decl post-processing 125s | |
| elaboration 11.8s | |
| elaboration: tactic compilation 292ms | |
| elaboration: tactic execution 8.41s | |
| parsing 388ms | |
| type checking 128ms | |
| src/group_theory/congruence.lean | |
| cumulative profiling times: | |
| compilation 111ms | |
| decl post-processing 129s | |
| elaboration 8.42s | |
| elaboration: tactic compilation 425ms | |
| elaboration: tactic execution 3.4s | |
| parsing 654ms | |
| type checking 148ms | |
| src/group_theory/coset.lean | |
| cumulative profiling times: | |
| compilation 12.3ms | |
| decl post-processing 39.5s | |
| elaboration 27.9s | |
| elaboration: tactic compilation 291ms | |
| elaboration: tactic execution 24s | |
| parsing 467ms | |
| type checking 17.3ms | |
| src/group_theory/eckmann_hilton.lean | |
| cumulative profiling times: | |
| compilation 12.2ms | |
| decl post-processing 9.7ms | |
| elaboration 498ms | |
| elaboration: tactic compilation 62.9ms | |
| elaboration: tactic execution 322ms | |
| parsing 102ms | |
| type checking 4.86ms | |
| src/group_theory/free_abelian_group.lean | |
| cumulative profiling times: | |
| compilation 110ms | |
| decl post-processing 279ms | |
| elaboration 18.4s | |
| elaboration: tactic compilation 542ms | |
| elaboration: tactic execution 11s | |
| parsing 1.29s | |
| type checking 220ms | |
| src/group_theory/free_group.lean | |
| cumulative profiling times: | |
| compilation 99.3ms | |
| decl post-processing 358ms | |
| elaboration 53s | |
| elaboration: tactic compilation 1.32s | |
| elaboration: tactic execution 54.3s | |
| parsing 2.86s | |
| type checking 250ms | |
| src/group_theory/group_action.lean | |
| cumulative profiling times: | |
| compilation 28.4ms | |
| decl post-processing 67.3ms | |
| elaboration 7.95s | |
| elaboration: tactic compilation 220ms | |
| elaboration: tactic execution 5.72s | |
| parsing 337ms | |
| type checking 28.9ms | |
| src/group_theory/monoid_localization.lean | |
| cumulative profiling times: | |
| compilation 36.3ms | |
| decl post-processing 180s | |
| elaboration 26.3s | |
| elaboration: tactic compilation 975ms | |
| elaboration: tactic execution 23.3s | |
| parsing 1.6s | |
| type checking 228ms | |
| src/group_theory/order_of_element.lean | |
| cumulative profiling times: | |
| compilation 20.5ms | |
| decl post-processing 26.4ms | |
| elaboration 54.2s | |
| elaboration: tactic compilation 1.22s | |
| elaboration: tactic execution 53s | |
| parsing 2s | |
| type checking 51.8ms | |
| src/group_theory/perm/cycles.lean | |
| cumulative profiling times: | |
| compilation 20.8ms | |
| decl post-processing 46.6ms | |
| elaboration 9.47s | |
| elaboration: tactic compilation 423ms | |
| elaboration: tactic execution 7.89s | |
| parsing 567ms | |
| type checking 11.7ms | |
| src/group_theory/perm/sign.lean | |
| cumulative profiling times: | |
| compilation 66.7ms | |
| decl post-processing 181ms | |
| elaboration 112s | |
| elaboration: tactic compilation 2.04s | |
| elaboration: tactic execution 99.9s | |
| parsing 3.96s | |
| type checking 101ms | |
| src/group_theory/presented_group.lean | |
| cumulative profiling times: | |
| compilation 6.95ms | |
| decl post-processing 16.5ms | |
| elaboration 203ms | |
| elaboration: tactic compilation 6.97ms | |
| elaboration: tactic execution 0ms | |
| parsing 4.58ms | |
| type checking 7.41ms | |
| src/group_theory/quotient_group.lean | |
| cumulative profiling times: | |
| compilation 31.7ms | |
| decl post-processing 22.6s | |
| elaboration 4.79s | |
| elaboration: tactic compilation 94.5ms | |
| elaboration: tactic execution 1.99s | |
| parsing 187ms | |
| type checking 68.4ms | |
| src/group_theory/subgroup.lean | |
| cumulative profiling times: | |
| compilation 33.6ms | |
| decl post-processing 83s | |
| elaboration 53.1s | |
| elaboration: tactic compilation 1.02s | |
| elaboration: tactic execution 42.7s | |
| parsing 1.73s | |
| type checking 99.7ms | |
| src/group_theory/submonoid.lean | |
| cumulative profiling times: | |
| compilation 145ms | |
| decl post-processing 125s | |
| elaboration 28s | |
| elaboration: tactic compilation 653ms | |
| elaboration: tactic execution 22.2s | |
| parsing 1.13s | |
| type checking 165ms | |
| src/group_theory/sylow.lean | |
| cumulative profiling times: | |
| compilation 55.4ms | |
| decl post-processing 32.7ms | |
| elaboration 23.5s | |
| elaboration: tactic compilation 550ms | |
| elaboration: tactic execution 20.4s | |
| parsing 996ms | |
| type checking 21.2ms | |
| src/linear_algebra/basic.lean | |
| cumulative profiling times: | |
| compilation 793ms | |
| decl post-processing 1.48s | |
| elaboration 268s | |
| elaboration: tactic compilation 3.48s | |
| elaboration: tactic execution 245s | |
| parsing 7.01s | |
| type checking 1.19s | |
| src/linear_algebra/basis.lean | |
| cumulative profiling times: | |
| compilation 0.885ms | |
| decl post-processing 128ms | |
| elaboration 212s | |
| elaboration: tactic compilation 2.83s | |
| elaboration: tactic execution 201s | |
| parsing 8.6s | |
| type checking 271ms | |
| src/linear_algebra/bilinear_form.lean | |
| cumulative profiling times: | |
| compilation 203ms | |
| decl post-processing 1.01s | |
| elaboration 42.6s | |
| elaboration: tactic compilation 890ms | |
| elaboration: tactic execution 30.7s | |
| parsing 1.68s | |
| type checking 925ms | |
| src/linear_algebra/contraction.lean | |
| cumulative profiling times: | |
| compilation 26.1ms | |
| decl post-processing 45.8ms | |
| elaboration 717ms | |
| elaboration: tactic compilation 37.7ms | |
| elaboration: tactic execution 189ms | |
| parsing 32.8ms | |
| type checking 27.6ms | |
| src/linear_algebra/default.lean | |
| src/linear_algebra/determinant.lean | |
| cumulative profiling times: | |
| compilation 22.9ms | |
| decl post-processing 27.8ms | |
| elaboration 48.3s | |
| elaboration: tactic compilation 657ms | |
| elaboration: tactic execution 51.9s | |
| parsing 1.66s | |
| type checking 14.9ms | |
| src/linear_algebra/dimension.lean | |
| cumulative profiling times: | |
| compilation 0.146ms | |
| decl post-processing 12.5ms | |
| elaboration 18.3s | |
| elaboration: tactic compilation 857ms | |
| elaboration: tactic execution 14s | |
| parsing 2.28s | |
| type checking 83ms | |
| src/linear_algebra/direct_sum_module.lean | |
| cumulative profiling times: | |
| compilation 47.8ms | |
| decl post-processing 126ms | |
| elaboration 1.43s | |
| elaboration: tactic compilation 71.3ms | |
| elaboration: tactic execution 315ms | |
| parsing 103ms | |
| type checking 95.9ms | |
| src/linear_algebra/dual.lean | |
| cumulative profiling times: | |
| compilation 29.9ms | |
| decl post-processing 310ms | |
| elaboration 32.9s | |
| elaboration: tactic compilation 558ms | |
| elaboration: tactic execution 24.9s | |
| parsing 1.59s | |
| type checking 568ms | |
| src/linear_algebra/finite_dimensional.lean | |
| cumulative profiling times: | |
| compilation 3.46ms | |
| decl post-processing 56.6ms | |
| elaboration 27.4s | |
| elaboration: tactic compilation 566ms | |
| elaboration: tactic execution 27.8s | |
| parsing 1.97s | |
| type checking 60.9ms | |
| src/linear_algebra/finsupp.lean | |
| cumulative profiling times: | |
| compilation 0.198ms | |
| decl post-processing 150ms | |
| elaboration 103s | |
| elaboration: tactic compilation 912ms | |
| elaboration: tactic execution 98.6s | |
| parsing 2.69s | |
| type checking 183ms | |
| src/linear_algebra/finsupp_vector_space.lean | |
| cumulative profiling times: | |
| compilation 0.0293ms | |
| decl post-processing 9.33ms | |
| elaboration 5.87s | |
| elaboration: tactic compilation 253ms | |
| elaboration: tactic execution 4.42s | |
| parsing 897ms | |
| type checking 11.2ms | |
| src/linear_algebra/linear_action.lean | |
| cumulative profiling times: | |
| compilation 14.2ms | |
| decl post-processing 38.5ms | |
| elaboration 13.4s | |
| elaboration: tactic compilation 178ms | |
| elaboration: tactic execution 17s | |
| parsing 450ms | |
| type checking 31ms | |
| src/linear_algebra/linear_pmap.lean | |
| cumulative profiling times: | |
| compilation 244ms | |
| decl post-processing 279ms | |
| elaboration 26.2s | |
| elaboration: tactic compilation 419ms | |
| elaboration: tactic execution 20.6s | |
| parsing 1.29s | |
| type checking 220ms | |
| src/linear_algebra/matrix.lean | |
| cumulative profiling times: | |
| compilation 74.8ms | |
| decl post-processing 166ms | |
| elaboration 49.2s | |
| elaboration: tactic compilation 570ms | |
| elaboration: tactic execution 46.3s | |
| parsing 1.79s | |
| type checking 183ms | |
| src/linear_algebra/multilinear.lean | |
| cumulative profiling times: | |
| compilation 262ms | |
| decl post-processing 565ms | |
| elaboration 104s | |
| elaboration: tactic compilation 1.4s | |
| elaboration: tactic execution 93.6s | |
| parsing 5.49s | |
| type checking 423ms | |
| src/linear_algebra/nonsingular_inverse.lean | |
| cumulative profiling times: | |
| compilation 34.3ms | |
| decl post-processing 33.4ms | |
| elaboration 34.1s | |
| elaboration: tactic compilation 869ms | |
| elaboration: tactic execution 35.6s | |
| parsing 2.14s | |
| type checking 34.9ms | |
| src/linear_algebra/quadratic_form.lean | |
| cumulative profiling times: | |
| compilation 77ms | |
| decl post-processing 130ms | |
| elaboration 91.8s | |
| elaboration: tactic compilation 585ms | |
| elaboration: tactic execution 83.3s | |
| parsing 1.1s | |
| type checking 104ms | |
| src/linear_algebra/sesquilinear_form.lean | |
| cumulative profiling times: | |
| compilation 144ms | |
| decl post-processing 897ms | |
| elaboration 7.96s | |
| elaboration: tactic compilation 561ms | |
| elaboration: tactic execution 2.37s | |
| parsing 957ms | |
| type checking 791ms | |
| src/linear_algebra/special_linear_group.lean | |
| cumulative profiling times: | |
| compilation 76.3ms | |
| decl post-processing 120ms | |
| elaboration 11.9s | |
| elaboration: tactic compilation 169ms | |
| elaboration: tactic execution 9.15s | |
| parsing 291ms | |
| type checking 56ms | |
| src/linear_algebra/tensor_product.lean | |
| cumulative profiling times: | |
| compilation 327ms | |
| decl post-processing 806ms | |
| elaboration 62.5s | |
| elaboration: tactic compilation 484ms | |
| elaboration: tactic execution 47.7s | |
| parsing 1.18s | |
| type checking 580ms | |
| src/logic/basic.lean | |
| cumulative profiling times: | |
| compilation 8.67ms | |
| decl post-processing 31.2ms | |
| elaboration 3.81s | |
| elaboration: tactic compilation 589ms | |
| elaboration: tactic execution 1.57s | |
| parsing 771ms | |
| type checking 20.6ms | |
| src/logic/embedding.lean | |
| cumulative profiling times: | |
| compilation 42.2ms | |
| decl post-processing 63.6ms | |
| elaboration 3.79s | |
| elaboration: tactic compilation 144ms | |
| elaboration: tactic execution 3.34s | |
| parsing 238ms | |
| type checking 17.4ms | |
| src/logic/function.lean | |
| cumulative profiling times: | |
| compilation 12.6ms | |
| decl post-processing 24.4ms | |
| elaboration 1.56s | |
| elaboration: tactic compilation 213ms | |
| elaboration: tactic execution 686ms | |
| parsing 403ms | |
| type checking 11.6ms | |
| src/logic/relation.lean | |
| cumulative profiling times: | |
| compilation 0.679ms | |
| decl post-processing 5.16ms | |
| elaboration 2.17s | |
| elaboration: tactic compilation 643ms | |
| elaboration: tactic execution 412ms | |
| parsing 1.46s | |
| type checking 6.33ms | |
| src/logic/relator.lean | |
| cumulative profiling times: | |
| compilation 1.24ms | |
| decl post-processing 9.82ms | |
| elaboration 76.1ms | |
| elaboration: tactic compilation 18.5ms | |
| elaboration: tactic execution 0ms | |
| parsing 20.5ms | |
| type checking 3.97ms | |
| src/logic/unique.lean | |
| cumulative profiling times: | |
| compilation 3.92ms | |
| decl post-processing 8.19ms | |
| elaboration 169ms | |
| elaboration: tactic compilation 42.9ms | |
| elaboration: tactic execution 9ms | |
| parsing 42.6ms | |
| type checking 2.44ms | |
| src/measure_theory/ae_eq_fun.lean | |
| cumulative profiling times: | |
| compilation 143ms | |
| decl post-processing 325ms | |
| elaboration 49.6s | |
| elaboration: tactic compilation 782ms | |
| elaboration: tactic execution 39.3s | |
| parsing 1.7s | |
| type checking 188ms | |
| src/measure_theory/bochner_integration.lean | |
| cumulative profiling times: | |
| compilation 21.1ms | |
| decl post-processing 995ms | |
| elaboration 56.9s | |
| elaboration: tactic compilation 2.43s | |
| elaboration: tactic execution 39.8s | |
| parsing 7.41s | |
| type checking 529ms | |
| src/measure_theory/borel_space.lean | |
| cumulative profiling times: | |
| compilation 14.7ms | |
| decl post-processing 14.6s | |
| elaboration 50.1s | |
| elaboration: tactic compilation 777ms | |
| elaboration: tactic execution 47.1s | |
| parsing 1.98s | |
| type checking 69.6ms | |
| src/measure_theory/category/Meas.lean | |
| cumulative profiling times: | |
| compilation 18.2ms | |
| decl post-processing 63.8ms | |
| elaboration 2.61s | |
| elaboration: tactic compilation 29.5ms | |
| elaboration: tactic execution 2ms | |
| parsing 20.5ms | |
| type checking 41ms | |
| src/measure_theory/decomposition.lean | |
| cumulative profiling times: | |
| compilation 0.0065ms | |
| decl post-processing 0.0101ms | |
| elaboration 10.6s | |
| elaboration: tactic compilation 302ms | |
| elaboration: tactic execution 12s | |
| parsing 2.06s | |
| type checking 2.66ms | |
| src/measure_theory/giry_monad.lean | |
| cumulative profiling times: | |
| compilation 0.0738ms | |
| decl post-processing 12.2ms | |
| elaboration 42.2s | |
| elaboration: tactic compilation 377ms | |
| elaboration: tactic execution 38.2s | |
| parsing 738ms | |
| type checking 8.83ms | |
| src/measure_theory/indicator_function.lean | |
| cumulative profiling times: | |
| compilation 0.0359ms | |
| decl post-processing 0.0478ms | |
| elaboration 3.42s | |
| elaboration: tactic compilation 333ms | |
| elaboration: tactic execution 2.26s | |
| parsing 1.41s | |
| type checking 4.51ms | |
| src/measure_theory/integration.lean | |
| cumulative profiling times: | |
| compilation 181ms | |
| decl post-processing 314ms | |
| elaboration 183s | |
| elaboration: tactic compilation 3.07s | |
| elaboration: tactic execution 164s | |
| parsing 10.5s | |
| type checking 177ms | |
| src/measure_theory/l1_space.lean | |
| cumulative profiling times: | |
| compilation 145ms | |
| decl post-processing 614ms | |
| elaboration 31.7s | |
| elaboration: tactic compilation 1.51s | |
| elaboration: tactic execution 20.9s | |
| parsing 3.05s | |
| type checking 291ms | |
| src/measure_theory/lebesgue_measure.lean | |
| cumulative profiling times: | |
| compilation 0.0868ms | |
| decl post-processing 9.97ms | |
| elaboration 94.5s | |
| elaboration: tactic compilation 670ms | |
| elaboration: tactic execution 116s | |
| parsing 1.91s | |
| type checking 11.2ms | |
| src/measure_theory/measurable_space.lean | |
| cumulative profiling times: | |
| compilation 199ms | |
| decl post-processing 249ms | |
| elaboration 46.9s | |
| elaboration: tactic compilation 1.3s | |
| elaboration: tactic execution 43.9s | |
| parsing 2.6s | |
| type checking 88.3ms | |
| src/measure_theory/measure_space.lean | |
| cumulative profiling times: | |
| compilation 18ms | |
| decl post-processing 214ms | |
| elaboration 108s | |
| elaboration: tactic compilation 1.55s | |
| elaboration: tactic execution 100s | |
| parsing 3.51s | |
| type checking 139ms | |
| src/measure_theory/outer_measure.lean | |
| cumulative profiling times: | |
| compilation 11.9ms | |
| decl post-processing 161ms | |
| elaboration 170s | |
| elaboration: tactic compilation 886ms | |
| elaboration: tactic execution 161s | |
| parsing 2.23s | |
| type checking 76.5ms | |
| src/measure_theory/probability_mass_function.lean | |
| cumulative profiling times: | |
| compilation 7ms | |
| decl post-processing 53.6ms | |
| elaboration 63.9s | |
| elaboration: tactic compilation 287ms | |
| elaboration: tactic execution 44.3s | |
| parsing 702ms | |
| type checking 9.31ms | |
| src/measure_theory/set_integral.lean | |
| cumulative profiling times: | |
| compilation 0.914ms | |
| decl post-processing 8.65ms | |
| elaboration 20.4s | |
| elaboration: tactic compilation 767ms | |
| elaboration: tactic execution 16.2s | |
| parsing 1.6s | |
| type checking 38ms | |
| src/measure_theory/simple_func_dense.lean | |
| cumulative profiling times: | |
| compilation 0.0067ms | |
| decl post-processing 0.0097ms | |
| elaboration 31.4s | |
| elaboration: tactic compilation 667ms | |
| elaboration: tactic execution 26.6s | |
| parsing 2.23s | |
| type checking 2.47ms | |
| src/meta/coinductive_predicates.lean | |
| cumulative profiling times: | |
| compilation 845ms | |
| decl post-processing 0.607ms | |
| elaboration 890ms | |
| elaboration: tactic compilation 0.464ms | |
| elaboration: tactic execution 0ms | |
| parsing 37.6ms | |
| type checking 29.7ms | |
| src/meta/expr.lean | |
| cumulative profiling times: | |
| compilation 404ms | |
| decl post-processing 11.5ms | |
| elaboration 1.46s | |
| parsing 35ms | |
| type checking 34.3ms | |
| src/meta/expr_lens.lean | |
| cumulative profiling times: | |
| compilation 28.7ms | |
| decl post-processing 1.26ms | |
| elaboration 151ms | |
| parsing 8.09ms | |
| type checking 1.62ms | |
| src/meta/rb_map.lean | |
| cumulative profiling times: | |
| compilation 71ms | |
| decl post-processing 0.841ms | |
| elaboration 99.8ms | |
| parsing 6.98ms | |
| type checking 7.1ms | |
| src/meta/uchange.lean | |
| cumulative profiling times: | |
| #eval execution 0ms | |
| compilation 14.2ms | |
| decl post-processing 0.473ms | |
| elaboration 28.2ms | |
| elaboration: tactic compilation 7.67ms | |
| elaboration: tactic execution 0ms | |
| parsing 1.06ms | |
| type checking 0.625ms | |
| src/number_theory/basic.lean | |
| cumulative profiling times: | |
| compilation 0.0036ms | |
| decl post-processing 0.0089ms | |
| elaboration 392ms | |
| elaboration: tactic compilation 28.8ms | |
| elaboration: tactic execution 293ms | |
| parsing 196ms | |
| type checking 0.833ms | |
| src/number_theory/bernoulli.lean | |
| cumulative profiling times: | |
| compilation 8.48ms | |
| decl post-processing 3.25ms | |
| elaboration 17.9s | |
| elaboration: tactic compilation 227ms | |
| elaboration: tactic execution 16.5s | |
| parsing 698ms | |
| type checking 3.56ms | |
| src/number_theory/dioph.lean | |
| cumulative profiling times: | |
| compilation 71.1ms | |
| decl post-processing 168ms | |
| elaboration 42.7s | |
| elaboration: tactic compilation 1.52s | |
| elaboration: tactic execution 43.1s | |
| parsing 2.35s | |
| type checking 41.9ms | |
| src/number_theory/pell.lean | |
| cumulative profiling times: | |
| compilation 14.4ms | |
| decl post-processing 49.5ms | |
| elaboration 38.7s | |
| elaboration: tactic compilation 2.82s | |
| elaboration: tactic execution 28.9s | |
| parsing 5.63s | |
| type checking 44.9ms | |
| src/number_theory/quadratic_reciprocity.lean | |
| cumulative profiling times: | |
| compilation 11.8ms | |
| decl post-processing 5.61ms | |
| elaboration 116s | |
| elaboration: tactic compilation 1.76s | |
| elaboration: tactic execution 122s | |
| parsing 4.46s | |
| type checking 25.5ms | |
| src/number_theory/sum_four_squares.lean | |
| cumulative profiling times: | |
| compilation 0.0153ms | |
| decl post-processing 0.0194ms | |
| elaboration 114s | |
| elaboration: tactic compilation 807ms | |
| elaboration: tactic execution 166s | |
| parsing 1.57s | |
| type checking 1.81ms | |
| src/number_theory/sum_two_squares.lean | |
| cumulative profiling times: | |
| compilation 0.0025ms | |
| decl post-processing 0.0099ms | |
| elaboration 3.38s | |
| elaboration: tactic compilation 9.37ms | |
| elaboration: tactic execution 3.15s | |
| parsing 28.3ms | |
| type checking 0.371ms | |
| src/order/basic.lean | |
| cumulative profiling times: | |
| compilation 86.2ms | |
| decl post-processing 228ms | |
| elaboration 5.7s | |
| elaboration: tactic compilation 674ms | |
| elaboration: tactic execution 2.38s | |
| parsing 904ms | |
| type checking 103ms | |
| src/order/boolean_algebra.lean | |
| cumulative profiling times: | |
| compilation 0.0545ms | |
| decl post-processing 3.65ms | |
| elaboration 1.42s | |
| elaboration: tactic compilation 69.2ms | |
| elaboration: tactic execution 1.02s | |
| parsing 142ms | |
| type checking 5.41ms | |
| src/order/bounded_lattice.lean | |
| cumulative profiling times: | |
| compilation 411ms | |
| decl post-processing 383ms | |
| elaboration 14.5s | |
| elaboration: tactic compilation 1.03s | |
| elaboration: tactic execution 8.16s | |
| parsing 2.01s | |
| type checking 267ms | |
| src/order/bounds.lean | |
| cumulative profiling times: | |
| compilation 1.6ms | |
| decl post-processing 13.8ms | |
| elaboration 5.37s | |
| elaboration: tactic compilation 447ms | |
| elaboration: tactic execution 3.15s | |
| parsing 782ms | |
| type checking 32.4ms | |
| src/order/complete_boolean_algebra.lean | |
| cumulative profiling times: | |
| compilation 25.1ms | |
| decl post-processing 6.57ms | |
| elaboration 44.9s | |
| elaboration: tactic compilation 204ms | |
| elaboration: tactic execution 42.9s | |
| parsing 689ms | |
| type checking 9.17ms | |
| src/order/complete_lattice.lean | |
| cumulative profiling times: | |
| compilation 133ms | |
| decl post-processing 182ms | |
| elaboration 17.2s | |
| elaboration: tactic compilation 619ms | |
| elaboration: tactic execution 12s | |
| parsing 1.03s | |
| type checking 188ms | |
| src/order/conditionally_complete_lattice.lean | |
| cumulative profiling times: | |
| compilation 69.8ms | |
| decl post-processing 235ms | |
| elaboration 19s | |
| elaboration: tactic compilation 1.23s | |
| elaboration: tactic execution 10.9s | |
| parsing 1.67s | |
| type checking 206ms | |
| src/order/copy.lean | |
| cumulative profiling times: | |
| compilation 94.6ms | |
| decl post-processing 184ms | |
| elaboration 2.5s | |
| elaboration: tactic compilation 72.2ms | |
| elaboration: tactic execution 1.25s | |
| parsing 50.3ms | |
| type checking 159ms | |
| src/order/default.lean | |
| src/order/filter/bases.lean | |
| cumulative profiling times: | |
| compilation 18.2ms | |
| decl post-processing 25.8ms | |
| elaboration 23.7s | |
| elaboration: tactic compilation 1.21s | |
| elaboration: tactic execution 18.2s | |
| parsing 2.47s | |
| type checking 28.4ms | |
| src/order/filter/basic.lean | |
| cumulative profiling times: | |
| compilation 177ms | |
| decl post-processing 416ms | |
| elaboration 98.9s | |
| elaboration: tactic compilation 3.89s | |
| elaboration: tactic execution 75.7s | |
| parsing 8.1s | |
| type checking 353ms | |
| src/order/filter/default.lean | |
| src/order/filter/extr.lean | |
| cumulative profiling times: | |
| compilation 1.44ms | |
| decl post-processing 7.93ms | |
| elaboration 1s | |
| parsing 24.8ms | |
| type checking 22.3ms | |
| src/order/filter/filter_product.lean | |
| cumulative profiling times: | |
| compilation 279ms | |
| decl post-processing 786ms | |
| elaboration 41.1s | |
| elaboration: tactic compilation 915ms | |
| elaboration: tactic execution 33s | |
| parsing 1.33s | |
| type checking 299ms | |
| src/order/filter/lift.lean | |
| cumulative profiling times: | |
| compilation 5.35ms | |
| decl post-processing 5.83ms | |
| elaboration 4.11s | |
| elaboration: tactic compilation 404ms | |
| elaboration: tactic execution 1.3s | |
| parsing 742ms | |
| type checking 26.6ms | |
| src/order/filter/partial.lean | |
| cumulative profiling times: | |
| compilation 13.4ms | |
| decl post-processing 32.6ms | |
| elaboration 30.2s | |
| elaboration: tactic compilation 313ms | |
| elaboration: tactic execution 27.6s | |
| parsing 581ms | |
| type checking 12.4ms | |
| src/order/filter/pointwise.lean | |
| cumulative profiling times: | |
| compilation 19ms | |
| decl post-processing 23s | |
| elaboration 9.56s | |
| elaboration: tactic compilation 329ms | |
| elaboration: tactic execution 7.93s | |
| parsing 623ms | |
| type checking 13.1ms | |
| src/order/fixed_points.lean | |
| cumulative profiling times: | |
| compilation 74.7ms | |
| decl post-processing 58.4ms | |
| elaboration 1.59s | |
| elaboration: tactic compilation 22.7ms | |
| elaboration: tactic execution 0ms | |
| parsing 16.6ms | |
| type checking 43.7ms | |
| src/order/galois_connection.lean | |
| cumulative profiling times: | |
| compilation 90.7ms | |
| decl post-processing 102ms | |
| elaboration 4.58s | |
| elaboration: tactic compilation 346ms | |
| elaboration: tactic execution 2.13s | |
| parsing 413ms | |
| type checking 80.7ms | |
| src/order/lattice.lean | |
| cumulative profiling times: | |
| compilation 106ms | |
| decl post-processing 132ms | |
| elaboration 32.6s | |
| elaboration: tactic compilation 716ms | |
| elaboration: tactic execution 28.1s | |
| parsing 1.62s | |
| type checking 109ms | |
| src/order/lexicographic.lean | |
| cumulative profiling times: | |
| compilation 104ms | |
| decl post-processing 92.8ms | |
| elaboration 4.36s | |
| elaboration: tactic compilation 516ms | |
| elaboration: tactic execution 763ms | |
| parsing 525ms | |
| type checking 38.9ms | |
| src/order/liminf_limsup.lean | |
| cumulative profiling times: | |
| compilation 27.1ms | |
| decl post-processing 33.1ms | |
| elaboration 27.1s | |
| elaboration: tactic compilation 495ms | |
| elaboration: tactic execution 23.9s | |
| parsing 725ms | |
| type checking 26.6ms | |
| src/order/order_iso.lean | |
| cumulative profiling times: | |
| compilation 51.5ms | |
| decl post-processing 80.3ms | |
| elaboration 12.6s | |
| elaboration: tactic compilation 440ms | |
| elaboration: tactic execution 9.48s | |
| parsing 794ms | |
| type checking 41.5ms | |
| src/order/pilex.lean | |
| cumulative profiling times: | |
| compilation 37.5ms | |
| decl post-processing 34.7ms | |
| elaboration 4.92s | |
| elaboration: tactic compilation 240ms | |
| elaboration: tactic execution 5.14s | |
| parsing 356ms | |
| type checking 16.1ms | |
| src/order/zorn.lean | |
| cumulative profiling times: | |
| compilation 1.26ms | |
| decl post-processing 9.68ms | |
| elaboration 6.58s | |
| elaboration: tactic compilation 382ms | |
| elaboration: tactic execution 4.8s | |
| parsing 1.15s | |
| type checking 10.2ms | |
| src/ring_theory/adjoin.lean | |
| cumulative profiling times: | |
| compilation 1.33ms | |
| decl post-processing 21.8ms | |
| elaboration 5.5s | |
| elaboration: tactic compilation 325ms | |
| elaboration: tactic execution 3.45s | |
| parsing 1.27s | |
| type checking 67.1ms | |
| src/ring_theory/adjoin_root.lean | |
| cumulative profiling times: | |
| compilation 1.22ms | |
| decl post-processing 188ms | |
| elaboration 24.3s | |
| elaboration: tactic compilation 92.3ms | |
| elaboration: tactic execution 9.14s | |
| parsing 161ms | |
| type checking 180ms | |
| src/ring_theory/algebra.lean | |
| cumulative profiling times: | |
| compilation 349ms | |
| decl post-processing 838ms | |
| elaboration 31.6s | |
| elaboration: tactic compilation 577ms | |
| elaboration: tactic execution 19.8s | |
| parsing 936ms | |
| type checking 532ms | |
| src/ring_theory/algebra_operations.lean | |
| cumulative profiling times: | |
| compilation 174ms | |
| decl post-processing 195ms | |
| elaboration 15.5s | |
| elaboration: tactic compilation 443ms | |
| elaboration: tactic execution 10.5s | |
| parsing 913ms | |
| type checking 183ms | |
| src/ring_theory/algebraic.lean | |
| cumulative profiling times: | |
| compilation 1.21ms | |
| decl post-processing 19.8ms | |
| elaboration 3.43s | |
| elaboration: tactic compilation 124ms | |
| elaboration: tactic execution 2.43s | |
| parsing 265ms | |
| type checking 91.2ms | |
| src/ring_theory/euclidean_domain.lean | |
| cumulative profiling times: | |
| compilation 0.0114ms | |
| decl post-processing 0.0146ms | |
| elaboration 8.5s | |
| elaboration: tactic compilation 111ms | |
| elaboration: tactic execution 8.17s | |
| parsing 287ms | |
| type checking 1.83ms | |
| src/ring_theory/fractional_ideal.lean | |
| cumulative profiling times: | |
| compilation 365ms | |
| decl post-processing 325ms | |
| elaboration 52s | |
| elaboration: tactic compilation 585ms | |
| elaboration: tactic execution 42.1s | |
| parsing 1.68s | |
| type checking 409ms | |
| src/ring_theory/free_comm_ring.lean | |
| cumulative profiling times: | |
| compilation 106ms | |
| decl post-processing 369ms | |
| elaboration 16.8s | |
| elaboration: tactic compilation 576ms | |
| elaboration: tactic execution 9.85s | |
| parsing 1.17s | |
| type checking 79.8ms | |
| src/ring_theory/free_ring.lean | |
| cumulative profiling times: | |
| compilation 21.7ms | |
| decl post-processing 23.4ms | |
| elaboration 818ms | |
| elaboration: tactic compilation 117ms | |
| elaboration: tactic execution 214ms | |
| parsing 260ms | |
| type checking 6.85ms | |
| src/ring_theory/ideal_operations.lean | |
| cumulative profiling times: | |
| compilation 167ms | |
| decl post-processing 283ms | |
| elaboration 15.5s | |
| elaboration: tactic compilation 554ms | |
| elaboration: tactic execution 5.4s | |
| parsing 1.25s | |
| type checking 410ms | |
| src/ring_theory/ideals.lean | |
| cumulative profiling times: | |
| compilation 118ms | |
| decl post-processing 272ms | |
| elaboration 49.4s | |
| elaboration: tactic compilation 597ms | |
| elaboration: tactic execution 31.1s | |
| parsing 1.26s | |
| type checking 209ms | |
| src/ring_theory/integral_closure.lean | |
| cumulative profiling times: | |
| compilation 3.63ms | |
| decl post-processing 15.6ms | |
| elaboration 36.9s | |
| elaboration: tactic compilation 688ms | |
| elaboration: tactic execution 32.3s | |
| parsing 3.71s | |
| type checking 173ms | |
| src/ring_theory/integral_domain.lean | |
| cumulative profiling times: | |
| compilation 0.541ms | |
| decl post-processing 12.6ms | |
| elaboration 20.6s | |
| elaboration: tactic compilation 275ms | |
| elaboration: tactic execution 20s | |
| parsing 689ms | |
| type checking 14.2ms | |
| src/ring_theory/localization.lean | |
| cumulative profiling times: | |
| compilation 248ms | |
| decl post-processing 508ms | |
| elaboration 144s | |
| elaboration: tactic compilation 1.15s | |
| elaboration: tactic execution 123s | |
| parsing 2.19s | |
| type checking 362ms | |
| src/ring_theory/maps.lean | |
| cumulative profiling times: | |
| compilation 18.4ms | |
| decl post-processing 25.2ms | |
| elaboration 347ms | |
| elaboration: tactic compilation 23.1ms | |
| elaboration: tactic execution 8ms | |
| parsing 32.7ms | |
| type checking 18.5ms | |
| src/ring_theory/multiplicity.lean | |
| cumulative profiling times: | |
| compilation 38.9ms | |
| decl post-processing 64ms | |
| elaboration 50.4s | |
| elaboration: tactic compilation 1.21s | |
| elaboration: tactic execution 44.6s | |
| parsing 2.3s | |
| type checking 31ms | |
| src/ring_theory/noetherian.lean | |
| cumulative profiling times: | |
| compilation 3.26ms | |
| decl post-processing 1.01s | |
| elaboration 45.2s | |
| elaboration: tactic compilation 1.11s | |
| elaboration: tactic execution 43.5s | |
| parsing 4.34s | |
| type checking 874ms | |
| src/ring_theory/polynomial.lean | |
| cumulative profiling times: | |
| compilation 22.8ms | |
| decl post-processing 152ms | |
| elaboration 42.7s | |
| elaboration: tactic compilation 453ms | |
| elaboration: tactic execution 15.2s | |
| parsing 1.51s | |
| type checking 119ms | |
| src/ring_theory/power_series.lean | |
| cumulative profiling times: | |
| compilation 23.2ms | |
| decl post-processing 1.28s | |
| elaboration 208s | |
| elaboration: tactic compilation 3.23s | |
| elaboration: tactic execution 171s | |
| parsing 8.75s | |
| type checking 321ms | |
| src/ring_theory/principal_ideal_domain.lean | |
| cumulative profiling times: | |
| compilation 1.57ms | |
| decl post-processing 36.9ms | |
| elaboration 48.4s | |
| elaboration: tactic compilation 294ms | |
| elaboration: tactic execution 52.5s | |
| parsing 638ms | |
| type checking 46.4ms | |
| src/ring_theory/subring.lean | |
| cumulative profiling times: | |
| compilation 95.1ms | |
| decl post-processing 138ms | |
| elaboration 2.89s | |
| elaboration: tactic compilation 360ms | |
| elaboration: tactic execution 1s | |
| parsing 821ms | |
| type checking 90.6ms | |
| src/ring_theory/unique_factorization_domain.lean | |
| cumulative profiling times: | |
| compilation 222ms | |
| decl post-processing 225ms | |
| elaboration 57.8s | |
| elaboration: tactic compilation 1.27s | |
| elaboration: tactic execution 48.6s | |
| parsing 2.62s | |
| type checking 213ms | |
| src/set_theory/cardinal.lean | |
| cumulative profiling times: | |
| compilation 46.1ms | |
| decl post-processing 294ms | |
| elaboration 89.4s | |
| elaboration: tactic compilation 2.36s | |
| elaboration: tactic execution 82.3s | |
| parsing 4.7s | |
| type checking 88.5ms | |
| src/set_theory/cofinality.lean | |
| cumulative profiling times: | |
| compilation 1.12ms | |
| decl post-processing 17ms | |
| elaboration 75.3s | |
| elaboration: tactic compilation 1.44s | |
| elaboration: tactic execution 74s | |
| parsing 4.04s | |
| type checking 15ms | |
| src/set_theory/game.lean | |
| cumulative profiling times: | |
| compilation 23.2ms | |
| decl post-processing 22.4ms | |
| elaboration 597ms | |
| elaboration: tactic compilation 142ms | |
| elaboration: tactic execution 60ms | |
| parsing 81.7ms | |
| type checking 11.7ms | |
| src/set_theory/game/domineering.lean | |
| cumulative profiling times: | |
| compilation 28.6ms | |
| decl post-processing 23.9ms | |
| elaboration 12.7s | |
| elaboration: tactic compilation 390ms | |
| elaboration: tactic execution 18.5s | |
| parsing 1.36s | |
| type checking 8.15ms | |
| src/set_theory/game/short.lean | |
| cumulative profiling times: | |
| compilation 185ms | |
| decl post-processing 392ms | |
| elaboration 18.2s | |
| elaboration: tactic compilation 693ms | |
| elaboration: tactic execution 2.53s | |
| parsing 475ms | |
| type checking 27.7ms | |
| src/set_theory/game/state.lean | |
| cumulative profiling times: | |
| compilation 79.9ms | |
| decl post-processing 333ms | |
| elaboration 6.8s | |
| elaboration: tactic compilation 292ms | |
| elaboration: tactic execution 3.05s | |
| parsing 545ms | |
| type checking 32.9ms | |
| src/set_theory/lists.lean | |
| cumulative profiling times: | |
| compilation 204ms | |
| decl post-processing 57.7ms | |
| elaboration 12.2s | |
| elaboration: tactic compilation 612ms | |
| elaboration: tactic execution 13.2s | |
| parsing 1.06s | |
| type checking 10.1ms | |
| src/set_theory/ordinal.lean | |
| cumulative profiling times: | |
| compilation 132ms | |
| decl post-processing 353ms | |
| elaboration 90.2s | |
| elaboration: tactic compilation 7.22s | |
| elaboration: tactic execution 55.2s | |
| parsing 16.9s | |
| type checking 236ms | |
| src/set_theory/ordinal_notation.lean | |
| cumulative profiling times: | |
| compilation 198ms | |
| decl post-processing 184ms | |
| elaboration 104s | |
| elaboration: tactic compilation 1.78s | |
| elaboration: tactic execution 91.1s | |
| parsing 7.44s | |
| type checking 36.3ms | |
| src/set_theory/pgame.lean | |
| cumulative profiling times: | |
| compilation 59.5ms | |
| decl post-processing 213ms | |
| elaboration 27.1s | |
| elaboration: tactic compilation 1.08s | |
| elaboration: tactic execution 9.87s | |
| parsing 2.56s | |
| type checking 32.9ms | |
| src/set_theory/schroeder_bernstein.lean | |
| cumulative profiling times: | |
| compilation 0.144ms | |
| decl post-processing 2.26ms | |
| elaboration 3.1s | |
| elaboration: tactic compilation 291ms | |
| elaboration: tactic execution 2.01s | |
| parsing 354ms | |
| type checking 0.773ms | |
| src/set_theory/surreal.lean | |
| cumulative profiling times: | |
| compilation 50.8ms | |
| decl post-processing 53.6ms | |
| elaboration 4.46s | |
| elaboration: tactic compilation 443ms | |
| elaboration: tactic execution 1.37s | |
| parsing 431ms | |
| type checking 11.6ms | |
| src/set_theory/zfc.lean | |
| cumulative profiling times: | |
| compilation 68.2ms | |
| decl post-processing 196ms | |
| elaboration 12.7s | |
| elaboration: tactic compilation 826ms | |
| elaboration: tactic execution 6.32s | |
| parsing 1.69s | |
| type checking 41.9ms | |
| src/tactic/abel.lean | |
| cumulative profiling times: | |
| compilation 226ms | |
| decl post-processing 8.18ms | |
| elaboration 11.3s | |
| elaboration: tactic compilation 214ms | |
| elaboration: tactic execution 8.05s | |
| parsing 434ms | |
| type checking 18.4ms | |
| src/tactic/algebra.lean | |
| cumulative profiling times: | |
| compilation 11.3ms | |
| decl post-processing 0.177ms | |
| elaboration 63.6ms | |
| elaboration: tactic compilation 0.347ms | |
| elaboration: tactic execution 0ms | |
| parsing 0.691ms | |
| type checking 1.12ms | |
| src/tactic/alias.lean | |
| cumulative profiling times: | |
| compilation 138ms | |
| decl post-processing 0.268ms | |
| elaboration 431ms | |
| elaboration: tactic compilation 0.512ms | |
| elaboration: tactic execution 0ms | |
| parsing 6.89ms | |
| type checking 8.23ms | |
| src/tactic/apply.lean | |
| cumulative profiling times: | |
| compilation 71.9ms | |
| decl post-processing 6.31ms | |
| elaboration 237ms | |
| parsing 6.22ms | |
| type checking 6.11ms | |
| src/tactic/apply_fun.lean | |
| cumulative profiling times: | |
| compilation 115ms | |
| decl post-processing 0.0072ms | |
| elaboration 140ms | |
| parsing 74.7ms | |
| type checking 5.58ms | |
| src/tactic/auto_cases.lean | |
| cumulative profiling times: | |
| compilation 79ms | |
| decl post-processing 0.0406ms | |
| elaboration 146ms | |
| parsing 6.14ms | |
| type checking 4.92ms | |
| src/tactic/basic.lean | |
| src/tactic/cache.lean | |
| cumulative profiling times: | |
| compilation 40.7ms | |
| decl post-processing 0.0286ms | |
| elaboration 181ms | |
| parsing 4.11ms | |
| type checking 43.7ms | |
| src/tactic/chain.lean | |
| cumulative profiling times: | |
| compilation 102ms | |
| decl post-processing 0.285ms | |
| elaboration 238ms | |
| parsing 8.86ms | |
| type checking 5.92ms | |
| src/tactic/clear.lean | |
| cumulative profiling times: | |
| compilation 41.9ms | |
| decl post-processing 0.0186ms | |
| elaboration 112ms | |
| parsing 21.1ms | |
| type checking 2.02ms | |
| src/tactic/converter/apply_congr.lean | |
| cumulative profiling times: | |
| compilation 44.4ms | |
| decl post-processing 0.0143ms | |
| elaboration 29.7ms | |
| parsing 13.3ms | |
| type checking 1.86ms | |
| src/tactic/converter/binders.lean | |
| cumulative profiling times: | |
| compilation 280ms | |
| decl post-processing 0.758ms | |
| elaboration 647ms | |
| elaboration: tactic compilation 23.7ms | |
| elaboration: tactic execution 2.47s | |
| parsing 57.4ms | |
| type checking 18ms | |
| src/tactic/converter/interactive.lean | |
| cumulative profiling times: | |
| compilation 131ms | |
| decl post-processing 0.051ms | |
| elaboration 257ms | |
| parsing 6.32ms | |
| type checking 41.1ms | |
| src/tactic/converter/old_conv.lean | |
| cumulative profiling times: | |
| compilation 308ms | |
| decl post-processing 0.246ms | |
| elaboration 548ms | |
| parsing 19.1ms | |
| type checking 20.2ms | |
| src/tactic/core.lean | |
| cumulative profiling times: | |
| compilation 1.66s | |
| decl post-processing 2.88ms | |
| elaboration 4.3s | |
| elaboration: tactic compilation 7.15ms | |
| elaboration: tactic execution 0ms | |
| parsing 118ms | |
| type checking 109ms | |
| src/tactic/default.lean | |
| src/tactic/derive_inhabited.lean | |
| cumulative profiling times: | |
| compilation 44.6ms | |
| decl post-processing 5.74ms | |
| elaboration 79.3ms | |
| parsing 2.22ms | |
| type checking 6.76ms | |
| src/tactic/doc_commands.lean | |
| cumulative profiling times: | |
| compilation 106ms | |
| decl post-processing 1.32ms | |
| elaboration 334ms | |
| elaboration: tactic compilation 1.16ms | |
| elaboration: tactic execution 0ms | |
| parsing 6.88ms | |
| type checking 12ms | |
| src/tactic/elide.lean | |
| cumulative profiling times: | |
| compilation 58.5ms | |
| decl post-processing 0.0639ms | |
| elaboration 203ms | |
| parsing 7.28ms | |
| type checking 3.53ms | |
| src/tactic/equiv_rw.lean | |
| cumulative profiling times: | |
| compilation 368ms | |
| decl post-processing 0.0273ms | |
| elaboration 813ms | |
| elaboration: tactic compilation 12.3ms | |
| elaboration: tactic execution 0ms | |
| parsing 56.1ms | |
| type checking 13.4ms | |
| src/tactic/explode.lean | |
| cumulative profiling times: | |
| compilation 88.3ms | |
| decl post-processing 1.88ms | |
| elaboration 177ms | |
| parsing 4.45ms | |
| type checking 6.16ms | |
| src/tactic/ext.lean | |
| cumulative profiling times: | |
| compilation 421ms | |
| decl post-processing 13.9ms | |
| elaboration 1.36s | |
| elaboration: tactic compilation 36.5ms | |
| elaboration: tactic execution 0ms | |
| parsing 67ms | |
| type checking 30ms | |
| src/tactic/fin_cases.lean | |
| cumulative profiling times: | |
| compilation 50ms | |
| decl post-processing 0.0233ms | |
| elaboration 701ms | |
| parsing 12ms | |
| type checking 18.3ms | |
| src/tactic/find.lean | |
| cumulative profiling times: | |
| compilation 115ms | |
| decl post-processing 0.109ms | |
| elaboration 476ms | |
| parsing 10.8ms | |
| type checking 5.5ms | |
| src/tactic/finish.lean | |
| cumulative profiling times: | |
| compilation 550ms | |
| decl post-processing 1.56ms | |
| elaboration 1.02s | |
| parsing 28.1ms | |
| type checking 26.9ms | |
| src/tactic/fix_reflect_string.lean | |
| cumulative profiling times: | |
| compilation 8.38ms | |
| decl post-processing 0.338ms | |
| elaboration 62.3ms | |
| elaboration: tactic compilation 10.4ms | |
| elaboration: tactic execution 0ms | |
| parsing 14.5ms | |
| type checking 1.52ms | |
| src/tactic/generalize_proofs.lean | |
| cumulative profiling times: | |
| compilation 9.35ms | |
| decl post-processing 0.0102ms | |
| elaboration 167ms | |
| parsing 3.37ms | |
| type checking 0.6ms | |
| src/tactic/hint.lean | |
| cumulative profiling times: | |
| compilation 34.1ms | |
| decl post-processing 0.341ms | |
| elaboration 104ms | |
| elaboration: tactic compilation 0.679ms | |
| elaboration: tactic execution 0ms | |
| parsing 4.15ms | |
| type checking 3.29ms | |
| src/tactic/interactive.lean | |
| cumulative profiling times: | |
| compilation 1.22s | |
| decl post-processing 1.5ms | |
| elaboration 2.24s | |
| parsing 66.6ms | |
| type checking 162ms | |
| src/tactic/interval_cases.lean | |
| cumulative profiling times: | |
| compilation 412ms | |
| decl post-processing 2.07ms | |
| elaboration 828ms | |
| parsing 40.3ms | |
| type checking 17.4ms | |
| src/tactic/lean_core_docs.lean | |
| src/tactic/lift.lean | |
| cumulative profiling times: | |
| compilation 342ms | |
| decl post-processing 3ms | |
| elaboration 383ms | |
| elaboration: tactic compilation 0.232ms | |
| elaboration: tactic execution 0ms | |
| parsing 8.09ms | |
| type checking 6.94ms | |
| src/tactic/linarith.lean | |
| cumulative profiling times: | |
| compilation 1.06s | |
| decl post-processing 21.3ms | |
| elaboration 22.5s | |
| elaboration: tactic compilation 314ms | |
| elaboration: tactic execution 5.82s | |
| parsing 734ms | |
| type checking 71.5ms | |
| src/tactic/lint/basic.lean | |
| cumulative profiling times: | |
| compilation 85.2ms | |
| decl post-processing 0.417ms | |
| elaboration 131ms | |
| elaboration: tactic compilation 1.2ms | |
| elaboration: tactic execution 0ms | |
| parsing 2.74ms | |
| type checking 4.15ms | |
| src/tactic/lint/default.lean | |
| cumulative profiling times: | |
| compilation 2.22ms | |
| decl post-processing 0.004ms | |
| elaboration 53.3ms | |
| elaboration: tactic compilation 11.4ms | |
| elaboration: tactic execution 0ms | |
| parsing 0.616ms | |
| type checking 0.123ms | |
| src/tactic/lint/frontend.lean | |
| cumulative profiling times: | |
| compilation 224ms | |
| decl post-processing 0.433ms | |
| elaboration 511ms | |
| parsing 9.91ms | |
| type checking 15ms | |
| src/tactic/lint/misc.lean | |
| cumulative profiling times: | |
| compilation 131ms | |
| decl post-processing 0.778ms | |
| elaboration 485ms | |
| parsing 4.43ms | |
| type checking 8.08ms | |
| src/tactic/lint/simp.lean | |
| cumulative profiling times: | |
| compilation 192ms | |
| decl post-processing 0.498ms | |
| elaboration 671ms | |
| parsing 18.4ms | |
| type checking 8.04ms | |
| src/tactic/lint/type_classes.lean | |
| cumulative profiling times: | |
| compilation 361ms | |
| decl post-processing 1.64ms | |
| elaboration 671ms | |
| parsing 11.4ms | |
| type checking 17.4ms | |
| src/tactic/local_cache.lean | |
| cumulative profiling times: | |
| compilation 110ms | |
| decl post-processing 4.05ms | |
| elaboration 445ms | |
| elaboration: tactic compilation 7.62ms | |
| elaboration: tactic execution 3ms | |
| parsing 13.4ms | |
| type checking 8.17ms | |
| src/tactic/localized.lean | |
| cumulative profiling times: | |
| compilation 39.6ms | |
| decl post-processing 0.33ms | |
| elaboration 108ms | |
| elaboration: tactic compilation 0.312ms | |
| elaboration: tactic execution 0ms | |
| parsing 1.82ms | |
| type checking 3.88ms | |
| src/tactic/mk_iff_of_inductive_prop.lean | |
| cumulative profiling times: | |
| compilation 308ms | |
| decl post-processing 4.81ms | |
| elaboration 491ms | |
| parsing 15ms | |
| type checking 16.7ms | |
| src/tactic/monotonicity/basic.lean | |
| cumulative profiling times: | |
| compilation 225ms | |
| decl post-processing 2.9ms | |
| elaboration 1.9s | |
| parsing 18.8ms | |
| type checking 15.3ms | |
| src/tactic/monotonicity/default.lean | |
| src/tactic/monotonicity/interactive.lean | |
| cumulative profiling times: | |
| compilation 1.32s | |
| decl post-processing 9.5ms | |
| elaboration 3.17s | |
| elaboration: tactic compilation 26.8ms | |
| elaboration: tactic execution 340ms | |
| parsing 126ms | |
| type checking 90.7ms | |
| src/tactic/monotonicity/lemmas.lean | |
| cumulative profiling times: | |
| compilation 0.0189ms | |
| decl post-processing 13.1ms | |
| elaboration 384ms | |
| elaboration: tactic compilation 101ms | |
| elaboration: tactic execution 35ms | |
| parsing 202ms | |
| type checking 1.52ms | |
| src/tactic/norm_cast.lean | |
| cumulative profiling times: | |
| compilation 1.35s | |
| decl post-processing 19.2ms | |
| elaboration 2.45s | |
| elaboration: tactic compilation 12.1ms | |
| elaboration: tactic execution 190ms | |
| parsing 64ms | |
| type checking 61.6ms | |
| src/tactic/norm_num.lean | |
| cumulative profiling times: | |
| compilation 2.09s | |
| decl post-processing 1.81ms | |
| elaboration 25.5s | |
| elaboration: tactic compilation 804ms | |
| elaboration: tactic execution 14.8s | |
| parsing 1.51s | |
| type checking 131ms | |
| src/tactic/nth_rewrite/basic.lean | |
| cumulative profiling times: | |
| compilation 2.8ms | |
| decl post-processing 0.0042ms | |
| elaboration 4.6ms | |
| parsing 0.245ms | |
| type checking 0.189ms | |
| src/tactic/nth_rewrite/congr.lean | |
| cumulative profiling times: | |
| compilation 102ms | |
| decl post-processing 0.0135ms | |
| elaboration 169ms | |
| parsing 4.14ms | |
| type checking 7.7ms | |
| src/tactic/nth_rewrite/default.lean | |
| cumulative profiling times: | |
| compilation 43.9ms | |
| decl post-processing 0.0305ms | |
| elaboration 86.1ms | |
| parsing 3.52ms | |
| type checking 4.69ms | |
| src/tactic/omega/clause.lean | |
| cumulative profiling times: | |
| compilation 2.49ms | |
| decl post-processing 7.69ms | |
| elaboration 196ms | |
| elaboration: tactic compilation 51ms | |
| elaboration: tactic execution 15ms | |
| parsing 106ms | |
| type checking 0.575ms | |
| src/tactic/omega/coeffs.lean | |
| cumulative profiling times: | |
| compilation 3.02ms | |
| decl post-processing 15.8ms | |
| elaboration 6.16s | |
| elaboration: tactic compilation 692ms | |
| elaboration: tactic execution 3.3s | |
| parsing 1.63s | |
| type checking 8.87ms | |
| src/tactic/omega/default.lean | |
| src/tactic/omega/eq_elim.lean | |
| cumulative profiling times: | |
| compilation 16.5ms | |
| decl post-processing 37ms | |
| elaboration 6.93s | |
| elaboration: tactic compilation 828ms | |
| elaboration: tactic execution 5.64s | |
| parsing 2.9s | |
| type checking 7.08ms | |
| src/tactic/omega/find_ees.lean | |
| cumulative profiling times: | |
| compilation 110ms | |
| decl post-processing 1.69ms | |
| elaboration 519ms | |
| parsing 6.22ms | |
| type checking 7.74ms | |
| src/tactic/omega/find_scalars.lean | |
| cumulative profiling times: | |
| compilation 12.3ms | |
| decl post-processing 0.0162ms | |
| elaboration 103ms | |
| parsing 2.66ms | |
| type checking 1.42ms | |
| src/tactic/omega/int/dnf.lean | |
| cumulative profiling times: | |
| compilation 1.72ms | |
| decl post-processing 32.8ms | |
| elaboration 2.85s | |
| elaboration: tactic compilation 372ms | |
| elaboration: tactic execution 1.36s | |
| parsing 665ms | |
| type checking 0.723ms | |
| src/tactic/omega/int/form.lean | |
| cumulative profiling times: | |
| compilation 17.6ms | |
| decl post-processing 25.3ms | |
| elaboration 354ms | |
| elaboration: tactic compilation 57.7ms | |
| elaboration: tactic execution 10ms | |
| parsing 137ms | |
| type checking 1.76ms | |
| src/tactic/omega/int/main.lean | |
| cumulative profiling times: | |
| compilation 101ms | |
| decl post-processing 0.0445ms | |
| elaboration 1.58s | |
| elaboration: tactic compilation 21.8ms | |
| elaboration: tactic execution 10ms | |
| parsing 47.7ms | |
| type checking 5.41ms | |
| src/tactic/omega/int/preterm.lean | |
| cumulative profiling times: | |
| compilation 1.47ms | |
| decl post-processing 13.7ms | |
| elaboration 321ms | |
| elaboration: tactic compilation 39.1ms | |
| elaboration: tactic execution 96ms | |
| parsing 93.7ms | |
| type checking 0.141ms | |
| src/tactic/omega/lin_comb.lean | |
| cumulative profiling times: | |
| compilation 0.402ms | |
| decl post-processing 4.95ms | |
| elaboration 477ms | |
| elaboration: tactic compilation 96ms | |
| elaboration: tactic execution 122ms | |
| parsing 186ms | |
| type checking 0.709ms | |
| src/tactic/omega/main.lean | |
| cumulative profiling times: | |
| compilation 33.4ms | |
| decl post-processing 0.0188ms | |
| elaboration 359ms | |
| parsing 5.79ms | |
| type checking 2.49ms | |
| src/tactic/omega/misc.lean | |
| cumulative profiling times: | |
| compilation 25ms | |
| decl post-processing 2.74ms | |
| elaboration 192ms | |
| elaboration: tactic compilation 56.7ms | |
| elaboration: tactic execution 1ms | |
| parsing 89.1ms | |
| type checking 1.36ms | |
| src/tactic/omega/nat/dnf.lean | |
| cumulative profiling times: | |
| compilation 4.85ms | |
| decl post-processing 17.7ms | |
| elaboration 2.84s | |
| elaboration: tactic compilation 180ms | |
| elaboration: tactic execution 2.06s | |
| parsing 424ms | |
| type checking 1.35ms | |
| src/tactic/omega/nat/form.lean | |
| cumulative profiling times: | |
| compilation 13.6ms | |
| decl post-processing 32.3ms | |
| elaboration 698ms | |
| elaboration: tactic compilation 134ms | |
| elaboration: tactic execution 62ms | |
| parsing 226ms | |
| type checking 1.43ms | |
| src/tactic/omega/nat/main.lean | |
| cumulative profiling times: | |
| compilation 142ms | |
| decl post-processing 0.0588ms | |
| elaboration 2.18s | |
| elaboration: tactic compilation 16.1ms | |
| elaboration: tactic execution 0ms | |
| parsing 50ms | |
| type checking 8.38ms | |
| src/tactic/omega/nat/neg_elim.lean | |
| cumulative profiling times: | |
| compilation 1.36ms | |
| decl post-processing 23.6ms | |
| elaboration 1.16s | |
| elaboration: tactic compilation 276ms | |
| elaboration: tactic execution 139ms | |
| parsing 428ms | |
| type checking 0.471ms | |
| src/tactic/omega/nat/preterm.lean | |
| cumulative profiling times: | |
| compilation 14.4ms | |
| decl post-processing 21.4ms | |
| elaboration 888ms | |
| elaboration: tactic compilation 91.3ms | |
| elaboration: tactic execution 353ms | |
| parsing 330ms | |
| type checking 2.19ms | |
| src/tactic/omega/nat/sub_elim.lean | |
| cumulative profiling times: | |
| compilation 6.99ms | |
| decl post-processing 22.2ms | |
| elaboration 1.37s | |
| elaboration: tactic compilation 229ms | |
| elaboration: tactic execution 399ms | |
| parsing 430ms | |
| type checking 0.848ms | |
| src/tactic/omega/prove_unsats.lean | |
| cumulative profiling times: | |
| compilation 42.7ms | |
| decl post-processing 0.0196ms | |
| elaboration 207ms | |
| parsing 2.17ms | |
| type checking 5.08ms | |
| src/tactic/omega/term.lean | |
| cumulative profiling times: | |
| compilation 9.67ms | |
| decl post-processing 61.5ms | |
| elaboration 680ms | |
| elaboration: tactic compilation 104ms | |
| elaboration: tactic execution 65ms | |
| parsing 291ms | |
| type checking 1.68ms | |
| src/tactic/pi_instances.lean | |
| cumulative profiling times: | |
| compilation 63.2ms | |
| decl post-processing 0.0094ms | |
| elaboration 148ms | |
| elaboration: tactic compilation 3.15ms | |
| elaboration: tactic execution 0ms | |
| parsing 1.9ms | |
| type checking 2.31ms | |
| src/tactic/push_neg.lean | |
| cumulative profiling times: | |
| compilation 188ms | |
| decl post-processing 0.0925ms | |
| elaboration 414ms | |
| parsing 60.1ms | |
| type checking 47.2ms | |
| src/tactic/rcases.lean | |
| cumulative profiling times: | |
| compilation 240ms | |
| decl post-processing 8.32ms | |
| elaboration 895ms | |
| elaboration: tactic compilation 16.4ms | |
| elaboration: tactic execution 0ms | |
| parsing 56.7ms | |
| type checking 660ms | |
| src/tactic/reassoc_axiom.lean | |
| cumulative profiling times: | |
| compilation 291ms | |
| decl post-processing 0.869ms | |
| elaboration 318ms | |
| elaboration: tactic compilation 0.275ms | |
| elaboration: tactic execution 0ms | |
| parsing 7.21ms | |
| type checking 14.1ms | |
| src/tactic/rename_var.lean | |
| cumulative profiling times: | |
| compilation 8.88ms | |
| decl post-processing 0.0205ms | |
| elaboration 36.5ms | |
| parsing 1.61ms | |
| type checking 1.19ms | |
| src/tactic/replacer.lean | |
| cumulative profiling times: | |
| compilation 68.5ms | |
| decl post-processing 0.246ms | |
| elaboration 339ms | |
| elaboration: tactic compilation 0.861ms | |
| elaboration: tactic execution 0ms | |
| parsing 17.4ms | |
| type checking 4.91ms | |
| src/tactic/restate_axiom.lean | |
| cumulative profiling times: | |
| compilation 49.5ms | |
| decl post-processing 0.0552ms | |
| elaboration 86ms | |
| parsing 2.99ms | |
| type checking 3.47ms | |
| src/tactic/rewrite.lean | |
| cumulative profiling times: | |
| compilation 182ms | |
| decl post-processing 0.0756ms | |
| elaboration 772ms | |
| parsing 18ms | |
| type checking 12.3ms | |
| src/tactic/rewrite_all/basic.lean | |
| cumulative profiling times: | |
| compilation 81.1ms | |
| decl post-processing 1.85ms | |
| elaboration 78.8ms | |
| parsing 3.27ms | |
| type checking 5.75ms | |
| src/tactic/ring.lean | |
| cumulative profiling times: | |
| compilation 284ms | |
| decl post-processing 17.5ms | |
| elaboration 16.3s | |
| elaboration: tactic compilation 224ms | |
| elaboration: tactic execution 12.2s | |
| parsing 493ms | |
| type checking 33.2ms | |
| src/tactic/ring2.lean | |
| cumulative profiling times: | |
| compilation 410ms | |
| decl post-processing 48.7ms | |
| elaboration 20.6s | |
| elaboration: tactic compilation 721ms | |
| elaboration: tactic execution 15.4s | |
| parsing 2.56s | |
| type checking 10.2ms | |
| src/tactic/ring_exp.lean | |
| cumulative profiling times: | |
| compilation 758ms | |
| decl post-processing 14.9ms | |
| elaboration 20s | |
| elaboration: tactic compilation 604ms | |
| elaboration: tactic execution 11s | |
| parsing 735ms | |
| type checking 88.3ms | |
| src/tactic/scc.lean | |
| cumulative profiling times: | |
| compilation 318ms | |
| decl post-processing 0.264ms | |
| elaboration 613ms | |
| parsing 19.1ms | |
| type checking 13.4ms | |
| src/tactic/show_term.lean | |
| cumulative profiling times: | |
| compilation 8.63ms | |
| decl post-processing 0.0055ms | |
| elaboration 7.24ms | |
| parsing 0.577ms | |
| type checking 0.29ms | |
| src/tactic/simp_command.lean | |
| cumulative profiling times: | |
| compilation 58.5ms | |
| decl post-processing 0.1ms | |
| elaboration 89.6ms | |
| parsing 2.22ms | |
| type checking 4.77ms | |
| src/tactic/simp_result.lean | |
| cumulative profiling times: | |
| compilation 28.5ms | |
| decl post-processing 0.0162ms | |
| elaboration 54.1ms | |
| parsing 1.72ms | |
| type checking 2.71ms | |
| src/tactic/simp_rw.lean | |
| cumulative profiling times: | |
| compilation 10.4ms | |
| decl post-processing 0.0073ms | |
| elaboration 17ms | |
| parsing 0.401ms | |
| type checking 0.97ms | |
| src/tactic/simpa.lean | |
| cumulative profiling times: | |
| compilation 60.4ms | |
| decl post-processing 0.0041ms | |
| elaboration 93.5ms | |
| parsing 1.22ms | |
| type checking 14ms | |
| src/tactic/simps.lean | |
| cumulative profiling times: | |
| compilation 40.7ms | |
| decl post-processing 0.181ms | |
| elaboration 1.11s | |
| elaboration: tactic compilation 0.303ms | |
| elaboration: tactic execution 0ms | |
| parsing 24.2ms | |
| type checking 2.6ms | |
| src/tactic/slice.lean | |
| cumulative profiling times: | |
| compilation 37.3ms | |
| decl post-processing 0.029ms | |
| elaboration 110ms | |
| parsing 3.01ms | |
| type checking 3.19ms | |
| src/tactic/solve_by_elim.lean | |
| cumulative profiling times: | |
| compilation 94ms | |
| decl post-processing 0.0246ms | |
| elaboration 293ms | |
| parsing 3.6ms | |
| type checking 4.88ms | |
| src/tactic/split_ifs.lean | |
| cumulative profiling times: | |
| compilation 63.4ms | |
| decl post-processing 0.0277ms | |
| elaboration 340ms | |
| elaboration: tactic compilation 8.8ms | |
| elaboration: tactic execution 7ms | |
| parsing 18.5ms | |
| type checking 3.85ms | |
| src/tactic/squeeze.lean | |
| cumulative profiling times: | |
| compilation 304ms | |
| decl post-processing 0.511ms | |
| elaboration 711ms | |
| elaboration: tactic compilation 4.16ms | |
| elaboration: tactic execution 0ms | |
| parsing 20.3ms | |
| type checking 42.5ms | |
| src/tactic/subtype_instance.lean | |
| cumulative profiling times: | |
| compilation 144ms | |
| decl post-processing 2.17ms | |
| elaboration 212ms | |
| parsing 33ms | |
| type checking 6.44ms | |
| src/tactic/suggest.lean | |
| cumulative profiling times: | |
| compilation 390ms | |
| decl post-processing 1.93ms | |
| elaboration 1.09s | |
| parsing 16.9ms | |
| type checking 32.2ms | |
| src/tactic/tauto.lean | |
| cumulative profiling times: | |
| compilation 209ms | |
| decl post-processing 0.0435ms | |
| elaboration 2.85s | |
| parsing 32ms | |
| type checking 20ms | |
| src/tactic/tfae.lean | |
| cumulative profiling times: | |
| compilation 109ms | |
| decl post-processing 0.0133ms | |
| elaboration 231ms | |
| parsing 7.1ms | |
| type checking 6.06ms | |
| src/tactic/tidy.lean | |
| cumulative profiling times: | |
| compilation 66.6ms | |
| decl post-processing 0.214ms | |
| elaboration 174ms | |
| elaboration: tactic compilation 3.01ms | |
| elaboration: tactic execution 0ms | |
| parsing 47.2ms | |
| type checking 3.75ms | |
| src/tactic/transfer.lean | |
| cumulative profiling times: | |
| compilation 130ms | |
| decl post-processing 0.203ms | |
| elaboration 668ms | |
| parsing 15.1ms | |
| type checking 20.3ms | |
| src/tactic/transform_decl.lean | |
| cumulative profiling times: | |
| compilation 9.08ms | |
| decl post-processing 0.0168ms | |
| elaboration 91ms | |
| parsing 2.12ms | |
| type checking 0.501ms | |
| src/tactic/transport.lean | |
| cumulative profiling times: | |
| compilation 69.1ms | |
| decl post-processing 1.71ms | |
| elaboration 140ms | |
| parsing 16.8ms | |
| type checking 3.2ms | |
| src/tactic/trunc_cases.lean | |
| cumulative profiling times: | |
| compilation 105ms | |
| decl post-processing 0.0201ms | |
| elaboration 186ms | |
| parsing 15.2ms | |
| type checking 5.16ms | |
| src/tactic/where.lean | |
| cumulative profiling times: | |
| compilation 90.8ms | |
| decl post-processing 3.3ms | |
| elaboration 309ms | |
| parsing 12.5ms | |
| type checking 7.41ms | |
| src/tactic/wlog.lean | |
| cumulative profiling times: | |
| compilation 413ms | |
| decl post-processing 0.0225ms | |
| elaboration 864ms | |
| parsing 16.4ms | |
| type checking 14.9ms | |
| src/topology/algebra/continuous_functions.lean | |
| cumulative profiling times: | |
| compilation 10.6ms | |
| decl post-processing 8.21s | |
| elaboration 362ms | |
| parsing 1.94ms | |
| type checking 45ms | |
| src/topology/algebra/group.lean | |
| cumulative profiling times: | |
| compilation 20.1ms | |
| decl post-processing 67.2s | |
| elaboration 42.4s | |
| elaboration: tactic compilation 699ms | |
| elaboration: tactic execution 36.9s | |
| parsing 2.07s | |
| type checking 44.3ms | |
| src/topology/algebra/group_completion.lean | |
| cumulative profiling times: | |
| compilation 2.65ms | |
| decl post-processing 117ms | |
| elaboration 10.9s | |
| elaboration: tactic compilation 89.1ms | |
| elaboration: tactic execution 8.72s | |
| parsing 125ms | |
| type checking 22.4ms | |
| src/topology/algebra/infinite_sum.lean | |
| cumulative profiling times: | |
| compilation 0.658ms | |
| decl post-processing 9.55ms | |
| elaboration 138s | |
| elaboration: tactic compilation 1.21s | |
| elaboration: tactic execution 72.4s | |
| parsing 3.83s | |
| type checking 41.2ms | |
| src/topology/algebra/module.lean | |
| cumulative profiling times: | |
| compilation 543ms | |
| decl post-processing 3.89s | |
| elaboration 87.5s | |
| elaboration: tactic compilation 509ms | |
| elaboration: tactic execution 75.5s | |
| parsing 1.17s | |
| type checking 568ms | |
| src/topology/algebra/monoid.lean | |
| cumulative profiling times: | |
| compilation 0.358ms | |
| decl post-processing 36.5s | |
| elaboration 16s | |
| elaboration: tactic compilation 97.2ms | |
| elaboration: tactic execution 14.4s | |
| parsing 135ms | |
| type checking 10.7ms | |
| src/topology/algebra/multilinear.lean | |
| cumulative profiling times: | |
| compilation 202ms | |
| decl post-processing 328ms | |
| elaboration 22.9s | |
| elaboration: tactic compilation 102ms | |
| elaboration: tactic execution 19.9s | |
| parsing 250ms | |
| type checking 191ms | |
| src/topology/algebra/open_subgroup.lean | |
| cumulative profiling times: | |
| compilation 49.1ms | |
| decl post-processing 55.5s | |
| elaboration 11.8s | |
| elaboration: tactic compilation 225ms | |
| elaboration: tactic execution 9.09s | |
| parsing 504ms | |
| type checking 29.7ms | |
| src/topology/algebra/ordered.lean | |
| cumulative profiling times: | |
| compilation 6.18ms | |
| decl post-processing 107ms | |
| elaboration 123s | |
| elaboration: tactic compilation 3.18s | |
| elaboration: tactic execution 128s | |
| parsing 7.5s | |
| type checking 213ms | |
| src/topology/algebra/polynomial.lean | |
| cumulative profiling times: | |
| compilation 0.008ms | |
| decl post-processing 0.0095ms | |
| elaboration 10.1s | |
| elaboration: tactic compilation 113ms | |
| elaboration: tactic execution 13.2s | |
| parsing 311ms | |
| type checking 1.44ms | |
| src/topology/algebra/ring.lean | |
| cumulative profiling times: | |
| compilation 7.91ms | |
| decl post-processing 42.7ms | |
| elaboration 4.19s | |
| elaboration: tactic compilation 106ms | |
| elaboration: tactic execution 6.15s | |
| parsing 136ms | |
| type checking 28.3ms | |
| src/topology/algebra/uniform_group.lean | |
| cumulative profiling times: | |
| compilation 8.39ms | |
| decl post-processing 40.7ms | |
| elaboration 53.7s | |
| elaboration: tactic compilation 823ms | |
| elaboration: tactic execution 44.2s | |
| parsing 3.91s | |
| type checking 71.4ms | |
| src/topology/algebra/uniform_ring.lean | |
| cumulative profiling times: | |
| compilation 22ms | |
| decl post-processing 148ms | |
| elaboration 21s | |
| elaboration: tactic compilation 223ms | |
| elaboration: tactic execution 5.62s | |
| parsing 408ms | |
| type checking 47.2ms | |
| src/topology/bases.lean | |
| cumulative profiling times: | |
| compilation 1.78ms | |
| decl post-processing 13.9ms | |
| elaboration 7.4s | |
| elaboration: tactic compilation 356ms | |
| elaboration: tactic execution 4.55s | |
| parsing 793ms | |
| type checking 8.67ms | |
| src/topology/basic.lean | |
| cumulative profiling times: | |
| compilation 9.31ms | |
| decl post-processing 52.2ms | |
| elaboration 31s | |
| elaboration: tactic compilation 1.36s | |
| elaboration: tactic execution 26.6s | |
| parsing 2.88s | |
| type checking 40.3ms | |
| src/topology/bounded_continuous_function.lean | |
| cumulative profiling times: | |
| compilation 148ms | |
| decl post-processing 379ms | |
| elaboration 76.6s | |
| elaboration: tactic compilation 835ms | |
| elaboration: tactic execution 83.2s | |
| parsing 2.09s | |
| type checking 193ms | |
| src/topology/category/Top/adjunctions.lean | |
| cumulative profiling times: | |
| compilation 52.6ms | |
| decl post-processing 105ms | |
| elaboration 52.4s | |
| elaboration: tactic compilation 20.3ms | |
| elaboration: tactic execution 49.2s | |
| parsing 9.8ms | |
| type checking 121ms | |
| src/topology/category/Top/basic.lean | |
| cumulative profiling times: | |
| compilation 36.6ms | |
| decl post-processing 32.6ms | |
| elaboration 209ms | |
| elaboration: tactic compilation 2ms | |
| elaboration: tactic execution 79ms | |
| parsing 0.912ms | |
| type checking 24ms | |
| src/topology/category/Top/default.lean | |
| src/topology/category/Top/epi_mono.lean | |
| cumulative profiling times: | |
| compilation 0.0071ms | |
| decl post-processing 0.0115ms | |
| elaboration 206ms | |
| elaboration: tactic compilation 59.7ms | |
| elaboration: tactic execution 48ms | |
| parsing 67.9ms | |
| type checking 2.3ms | |
| src/topology/category/Top/limits.lean | |
| cumulative profiling times: | |
| compilation 167ms | |
| decl post-processing 122ms | |
| elaboration 1.76s | |
| elaboration: tactic compilation 63.4ms | |
| elaboration: tactic execution 276ms | |
| parsing 14.9ms | |
| type checking 90.5ms | |
| src/topology/category/Top/open_nhds.lean | |
| cumulative profiling times: | |
| compilation 67.8ms | |
| decl post-processing 108ms | |
| elaboration 9s | |
| elaboration: tactic compilation 142ms | |
| elaboration: tactic execution 7.52s | |
| parsing 178ms | |
| type checking 143ms | |
| src/topology/category/Top/opens.lean | |
| cumulative profiling times: | |
| compilation 111ms | |
| decl post-processing 128ms | |
| elaboration 21s | |
| elaboration: tactic compilation 114ms | |
| elaboration: tactic execution 19.1s | |
| parsing 124ms | |
| type checking 145ms | |
| src/topology/category/TopCommRing.lean | |
| cumulative profiling times: | |
| compilation 48.5ms | |
| decl post-processing 166ms | |
| elaboration 16.7s | |
| elaboration: tactic compilation 23.6ms | |
| elaboration: tactic execution 15.3s | |
| parsing 45.3ms | |
| type checking 122ms | |
| src/topology/category/UniformSpace.lean | |
| cumulative profiling times: | |
| compilation 41.7ms | |
| decl post-processing 133ms | |
| elaboration 54.2s | |
| elaboration: tactic compilation 157ms | |
| elaboration: tactic execution 50.3s | |
| parsing 208ms | |
| type checking 102ms | |
| src/topology/compact_open.lean | |
| cumulative profiling times: | |
| compilation 16.8ms | |
| decl post-processing 20.6ms | |
| elaboration 9.25s | |
| elaboration: tactic compilation 138ms | |
| elaboration: tactic execution 8.31s | |
| parsing 250ms | |
| type checking 9.58ms | |
| src/topology/constructions.lean | |
| cumulative profiling times: | |
| compilation 29.3ms | |
| decl post-processing 47.4ms | |
| elaboration 30.8s | |
| elaboration: tactic compilation 1.21s | |
| elaboration: tactic execution 24.5s | |
| parsing 4.04s | |
| type checking 56.5ms | |
| src/topology/continuous_on.lean | |
| cumulative profiling times: | |
| compilation 5.96ms | |
| decl post-processing 6.44ms | |
| elaboration 23.7s | |
| elaboration: tactic compilation 829ms | |
| elaboration: tactic execution 19.7s | |
| parsing 2.14s | |
| type checking 30.2ms | |
| src/topology/dense_embedding.lean | |
| cumulative profiling times: | |
| compilation 3.06ms | |
| decl post-processing 11.2ms | |
| elaboration 11.8s | |
| elaboration: tactic compilation 267ms | |
| elaboration: tactic execution 9.92s | |
| parsing 953ms | |
| type checking 14ms | |
| src/topology/homeomorph.lean | |
| cumulative profiling times: | |
| compilation 45.1ms | |
| decl post-processing 50.4ms | |
| elaboration 2.66s | |
| elaboration: tactic compilation 149ms | |
| elaboration: tactic execution 1.71s | |
| parsing 317ms | |
| type checking 27.2ms | |
| src/topology/instances/complex.lean | |
| cumulative profiling times: | |
| compilation 1.06ms | |
| decl post-processing 29.7ms | |
| elaboration 7.22s | |
| elaboration: tactic compilation 124ms | |
| elaboration: tactic execution 5.52s | |
| parsing 241ms | |
| type checking 32.6ms | |
| src/topology/instances/ennreal.lean | |
| cumulative profiling times: | |
| compilation 4.18ms | |
| decl post-processing 325ms | |
| elaboration 116s | |
| elaboration: tactic compilation 2.45s | |
| elaboration: tactic execution 123s | |
| parsing 6.28s | |
| type checking 109ms | |
| src/topology/instances/nnreal.lean | |
| cumulative profiling times: | |
| compilation 0.914ms | |
| decl post-processing 293ms | |
| elaboration 13s | |
| elaboration: tactic compilation 94.4ms | |
| elaboration: tactic execution 9.76s | |
| parsing 293ms | |
| type checking 46.4ms | |
| src/topology/instances/real.lean | |
| cumulative profiling times: | |
| compilation 2.8ms | |
| decl post-processing 161ms | |
| elaboration 37s | |
| elaboration: tactic compilation 605ms | |
| elaboration: tactic execution 33.4s | |
| parsing 1.58s | |
| type checking 78.3ms | |
| src/topology/instances/real_vector_space.lean | |
| cumulative profiling times: | |
| compilation 8.48ms | |
| decl post-processing 21.2ms | |
| elaboration 562ms | |
| parsing 0.999ms | |
| type checking 28.1ms | |
| src/topology/list.lean | |
| cumulative profiling times: | |
| compilation 4.8ms | |
| decl post-processing 4.58ms | |
| elaboration 13.3s | |
| elaboration: tactic compilation 409ms | |
| elaboration: tactic execution 10.6s | |
| parsing 1.12s | |
| type checking 7.5ms | |
| src/topology/local_extr.lean | |
| cumulative profiling times: | |
| compilation 1.66ms | |
| decl post-processing 8.83ms | |
| elaboration 373ms | |
| parsing 21.4ms | |
| type checking 25.2ms | |
| src/topology/local_homeomorph.lean | |
| cumulative profiling times: | |
| compilation 92.9ms | |
| decl post-processing 154ms | |
| elaboration 32.7s | |
| elaboration: tactic compilation 854ms | |
| elaboration: tactic execution 34.9s | |
| parsing 2.3s | |
| type checking 116ms | |
| src/topology/maps.lean | |
| cumulative profiling times: | |
| compilation 0.944ms | |
| decl post-processing 5.34ms | |
| elaboration 13s | |
| elaboration: tactic compilation 709ms | |
| elaboration: tactic execution 10.1s | |
| parsing 1.2s | |
| type checking 13.9ms | |
| src/topology/metric_space/antilipschitz.lean | |
| cumulative profiling times: | |
| compilation 2.89ms | |
| decl post-processing 12.4ms | |
| elaboration 9.47s | |
| elaboration: tactic compilation 201ms | |
| elaboration: tactic execution 8.16s | |
| parsing 487ms | |
| type checking 6.62ms | |
| src/topology/metric_space/baire.lean | |
| cumulative profiling times: | |
| compilation 0.361ms | |
| decl post-processing 2.06ms | |
| elaboration 26.5s | |
| elaboration: tactic compilation 815ms | |
| elaboration: tactic execution 28.7s | |
| parsing 3.32s | |
| type checking 6.41ms | |
| src/topology/metric_space/basic.lean | |
| cumulative profiling times: | |
| compilation 54.2ms | |
| decl post-processing 287ms | |
| elaboration 147s | |
| elaboration: tactic compilation 3.57s | |
| elaboration: tactic execution 139s | |
| parsing 8.73s | |
| type checking 222ms | |
| src/topology/metric_space/cau_seq_filter.lean | |
| cumulative profiling times: | |
| compilation 0.767ms | |
| decl post-processing 47ms | |
| elaboration 41s | |
| elaboration: tactic compilation 171ms | |
| elaboration: tactic execution 38.3s | |
| parsing 570ms | |
| type checking 39ms | |
| src/topology/metric_space/closeds.lean | |
| cumulative profiling times: | |
| compilation 2.37ms | |
| decl post-processing 396ms | |
| elaboration 33.3s | |
| elaboration: tactic compilation 813ms | |
| elaboration: tactic execution 39.8s | |
| parsing 4.43s | |
| type checking 349ms | |
| src/topology/metric_space/completion.lean | |
| cumulative profiling times: | |
| compilation 0.0587ms | |
| decl post-processing 10.5ms | |
| elaboration 27.8s | |
| elaboration: tactic compilation 323ms | |
| elaboration: tactic execution 25.4s | |
| parsing 1.45s | |
| type checking 6.56ms | |
| src/topology/metric_space/contracting.lean | |
| cumulative profiling times: | |
| compilation 0.362ms | |
| decl post-processing 28ms | |
| elaboration 11.7s | |
| elaboration: tactic compilation 356ms | |
| elaboration: tactic execution 9.34s | |
| parsing 756ms | |
| type checking 40.1ms | |
| src/topology/metric_space/emetric_space.lean | |
| cumulative profiling times: | |
| compilation 34.4ms | |
| decl post-processing 100ms | |
| elaboration 71.5s | |
| elaboration: tactic compilation 1.63s | |
| elaboration: tactic execution 71.5s | |
| parsing 4.19s | |
| type checking 88.7ms | |
| src/topology/metric_space/gluing.lean | |
| cumulative profiling times: | |
| compilation 3.36ms | |
| decl post-processing 206ms | |
| elaboration 67.9s | |
| elaboration: tactic compilation 1.51s | |
| elaboration: tactic execution 88.1s | |
| parsing 5.09s | |
| type checking 60.7ms | |
| src/topology/metric_space/gromov_hausdorff.lean | |
| cumulative profiling times: | |
| compilation 40.3ms | |
| decl post-processing 1.09s | |
| elaboration 128s | |
| elaboration: tactic compilation 2.68s | |
| elaboration: tactic execution 145s | |
| parsing 16.5s | |
| type checking 1.36s | |
| src/topology/metric_space/gromov_hausdorff_realized.lean | |
| cumulative profiling times: | |
| compilation 3.87ms | |
| decl post-processing 143ms | |
| elaboration 69.6s | |
| elaboration: tactic compilation 1.09s | |
| elaboration: tactic execution 80.4s | |
| parsing 4.02s | |
| type checking 83.7ms | |
| src/topology/metric_space/hausdorff_distance.lean | |
| cumulative profiling times: | |
| compilation 0.257ms | |
| decl post-processing 26.9ms | |
| elaboration 270s | |
| elaboration: tactic compilation 2.44s | |
| elaboration: tactic execution 300s | |
| parsing 6.67s | |
| type checking 50.9ms | |
| src/topology/metric_space/isometry.lean | |
| cumulative profiling times: | |
| compilation 71ms | |
| decl post-processing 117ms | |
| elaboration 30.7s | |
| elaboration: tactic compilation 414ms | |
| elaboration: tactic execution 33.4s | |
| parsing 1.02s | |
| type checking 49.6ms | |
| src/topology/metric_space/lipschitz.lean | |
| cumulative profiling times: | |
| compilation 0.761ms | |
| decl post-processing 3.65ms | |
| elaboration 9.51s | |
| elaboration: tactic compilation 390ms | |
| elaboration: tactic execution 7.33s | |
| parsing 800ms | |
| type checking 21.8ms | |
| src/topology/metric_space/premetric_space.lean | |
| cumulative profiling times: | |
| compilation 12.8ms | |
| decl post-processing 27.5ms | |
| elaboration 9.5s | |
| elaboration: tactic compilation 251ms | |
| elaboration: tactic execution 14.2s | |
| parsing 401ms | |
| type checking 15.7ms | |
| src/topology/opens.lean | |
| cumulative profiling times: | |
| compilation 88.8ms | |
| decl post-processing 102ms | |
| elaboration 8.39s | |
| elaboration: tactic compilation 238ms | |
| elaboration: tactic execution 6.76s | |
| parsing 497ms | |
| type checking 33.2ms | |
| src/topology/order.lean | |
| cumulative profiling times: | |
| compilation 93.8ms | |
| decl post-processing 86ms | |
| elaboration 14s | |
| elaboration: tactic compilation 770ms | |
| elaboration: tactic execution 9.73s | |
| parsing 1.28s | |
| type checking 52.5ms | |
| src/topology/separation.lean | |
| cumulative profiling times: | |
| compilation 3.89ms | |
| decl post-processing 78.3ms | |
| elaboration 15.8s | |
| elaboration: tactic compilation 417ms | |
| elaboration: tactic execution 12.7s | |
| parsing 834ms | |
| type checking 49.8ms | |
| src/topology/sequences.lean | |
| cumulative profiling times: | |
| compilation 1.14ms | |
| decl post-processing 17.3ms | |
| elaboration 5.54s | |
| elaboration: tactic compilation 301ms | |
| elaboration: tactic execution 4.3s | |
| parsing 143ms | |
| type checking 5.03ms | |
| src/topology/sheaves/presheaf.lean | |
| cumulative profiling times: | |
| compilation 38.6ms | |
| decl post-processing 114ms | |
| elaboration 28s | |
| elaboration: tactic compilation 195ms | |
| elaboration: tactic execution 25.8s | |
| parsing 180ms | |
| type checking 129ms | |
| src/topology/sheaves/presheaf_of_functions.lean | |
| cumulative profiling times: | |
| compilation 215ms | |
| decl post-processing 792ms | |
| elaboration 24.8s | |
| elaboration: tactic compilation 182ms | |
| elaboration: tactic execution 21.1s | |
| parsing 227ms | |
| type checking 1.13s | |
| src/topology/sheaves/stalks.lean | |
| cumulative profiling times: | |
| compilation 55.2ms | |
| decl post-processing 68.9ms | |
| elaboration 10.8s | |
| elaboration: tactic compilation 77.8ms | |
| elaboration: tactic execution 9.91s | |
| parsing 203ms | |
| type checking 102ms | |
| src/topology/stone_cech.lean | |
| cumulative profiling times: | |
| compilation 9.62ms | |
| decl post-processing 51.9ms | |
| elaboration 4.68s | |
| elaboration: tactic compilation 399ms | |
| elaboration: tactic execution 2.7s | |
| parsing 1.23s | |
| type checking 25.3ms | |
| src/topology/subset_properties.lean | |
| cumulative profiling times: | |
| compilation 19.3ms | |
| decl post-processing 85.9ms | |
| elaboration 90.2s | |
| elaboration: tactic compilation 3.28s | |
| elaboration: tactic execution 76.9s | |
| parsing 8.2s | |
| type checking 69.2ms | |
| src/topology/topological_fiber_bundle.lean | |
| cumulative profiling times: | |
| compilation 106ms | |
| decl post-processing 144ms | |
| elaboration 48.2s | |
| elaboration: tactic compilation 770ms | |
| elaboration: tactic execution 48.8s | |
| parsing 2.23s | |
| type checking 88.2ms | |
| src/topology/uniform_space/absolute_value.lean | |
| cumulative profiling times: | |
| compilation 14.3ms | |
| decl post-processing 13.3ms | |
| elaboration 6.7s | |
| elaboration: tactic compilation 102ms | |
| elaboration: tactic execution 6.43s | |
| parsing 203ms | |
| type checking 6.32ms | |
| src/topology/uniform_space/abstract_completion.lean | |
| cumulative profiling times: | |
| compilation 6.6ms | |
| decl post-processing 26.1ms | |
| elaboration 981ms | |
| elaboration: tactic compilation 155ms | |
| elaboration: tactic execution 191ms | |
| parsing 352ms | |
| type checking 21.1ms | |
| src/topology/uniform_space/basic.lean | |
| cumulative profiling times: | |
| compilation 425ms | |
| decl post-processing 238ms | |
| elaboration 78.3s | |
| elaboration: tactic compilation 2.37s | |
| elaboration: tactic execution 65.6s | |
| parsing 4.62s | |
| type checking 180ms | |
| src/topology/uniform_space/cauchy.lean | |
| cumulative profiling times: | |
| compilation 2.39ms | |
| decl post-processing 48.4ms | |
| elaboration 22s | |
| elaboration: tactic compilation 674ms | |
| elaboration: tactic execution 17.4s | |
| parsing 1.58s | |
| type checking 38.1ms | |
| src/topology/uniform_space/compare_reals.lean | |
| cumulative profiling times: | |
| compilation 2.87ms | |
| decl post-processing 47.1ms | |
| elaboration 2.74s | |
| elaboration: tactic compilation 156ms | |
| elaboration: tactic execution 2.61s | |
| parsing 139ms | |
| type checking 39.8ms | |
| src/topology/uniform_space/complete_separated.lean | |
| cumulative profiling times: | |
| compilation 0.0066ms | |
| decl post-processing 0.0136ms | |
| elaboration 111ms | |
| elaboration: tactic compilation 18.5ms | |
| elaboration: tactic execution 49ms | |
| parsing 89.1ms | |
| type checking 0.773ms | |
| src/topology/uniform_space/completion.lean | |
| cumulative profiling times: | |
| compilation 24.8ms | |
| decl post-processing 77.2ms | |
| elaboration 18.8s | |
| elaboration: tactic compilation 521ms | |
| elaboration: tactic execution 13.6s | |
| parsing 1.03s | |
| type checking 50.1ms | |
| src/topology/uniform_space/pi.lean | |
| cumulative profiling times: | |
| compilation 5.08ms | |
| decl post-processing 79.2ms | |
| elaboration 775ms | |
| elaboration: tactic compilation 52.5ms | |
| elaboration: tactic execution 203ms | |
| parsing 195ms | |
| type checking 36.9ms | |
| src/topology/uniform_space/separation.lean | |
| cumulative profiling times: | |
| compilation 15.5ms | |
| decl post-processing 54.5ms | |
| elaboration 36.6s | |
| elaboration: tactic compilation 494ms | |
| elaboration: tactic execution 31.8s | |
| parsing 1.24s | |
| type checking 28.8ms | |
| src/topology/uniform_space/uniform_convergence.lean | |
| cumulative profiling times: | |
| compilation 1.94ms | |
| decl post-processing 17.3ms | |
| elaboration 19.9s | |
| elaboration: tactic compilation 402ms | |
| elaboration: tactic execution 17.5s | |
| parsing 1.13s | |
| type checking 19.8ms | |
| src/topology/uniform_space/uniform_embedding.lean | |
| cumulative profiling times: | |
| compilation 0.092ms | |
| decl post-processing 0.134ms | |
| elaboration 21.7s | |
| elaboration: tactic compilation 667ms | |
| elaboration: tactic execution 20.3s | |
| parsing 1.54s | |
| type checking 16.2ms | |
| test/abel.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 35ms | |
| elaboration: tactic execution 561ms | |
| parsing 55.9ms | |
| test/apply.lean | |
| cumulative profiling times: | |
| compilation 2.7ms | |
| decl post-processing 2.97ms | |
| elaboration 3.54s | |
| elaboration: tactic compilation 92.9ms | |
| elaboration: tactic execution 3.33s | |
| parsing 85.9ms | |
| type checking 1.22ms | |
| test/apply_fun.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 69.5ms | |
| elaboration: tactic execution 4.39s | |
| parsing 162ms | |
| test/back_chaining.lean | |
| cumulative profiling times: | |
| compilation 0.0131ms | |
| decl post-processing 0.103ms | |
| elaboration 306ms | |
| elaboration: tactic compilation 27.3ms | |
| elaboration: tactic execution 205ms | |
| parsing 34.8ms | |
| type checking 0.86ms | |
| test/choose.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 65ms | |
| elaboration: tactic execution 10ms | |
| parsing 143ms | |
| test/coinductive.lean | |
| cumulative profiling times: | |
| compilation 0.0022ms | |
| decl post-processing 0.0193ms | |
| elaboration 12.7ms | |
| elaboration: tactic compilation 52ms | |
| elaboration: tactic execution 15ms | |
| parsing 140ms | |
| type checking 0.101ms | |
| test/conv.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 206ms | |
| elaboration: tactic execution 8.5s | |
| parsing 676ms | |
| test/conv/apply_congr.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 283ms | |
| elaboration: tactic execution 14.1s | |
| parsing 676ms | |
| test/conv/conv.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 156ms | |
| elaboration: tactic execution 917ms | |
| parsing 328ms | |
| test/convert.lean | |
| cumulative profiling times: | |
| compilation 0.0032ms | |
| decl post-processing 0.285ms | |
| elaboration 267ms | |
| elaboration: tactic compilation 38.4ms | |
| elaboration: tactic execution 701ms | |
| parsing 129ms | |
| type checking 0.163ms | |
| test/delta_instance.lean | |
| cumulative profiling times: | |
| compilation 1.61ms | |
| decl post-processing 63.1ms | |
| elaboration 1.09ms | |
| parsing 0.402ms | |
| type checking 0.145ms | |
| test/differentiable.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 753ms | |
| elaboration: tactic execution 51.5s | |
| parsing 965ms | |
| test/doc_commands.lean | |
| cumulative profiling times: | |
| #eval execution 0ms | |
| compilation 0.291ms | |
| decl post-processing 0.337ms | |
| elaboration 0.599ms | |
| parsing 0.0348ms | |
| type checking 0.0539ms | |
| test/equiv_rw.lean | |
| cumulative profiling times: | |
| compilation 9.2ms | |
| decl post-processing 11.3ms | |
| elaboration 2.75s | |
| elaboration: tactic compilation 582ms | |
| elaboration: tactic execution 3.84s | |
| parsing 1.46s | |
| type checking 6.38ms | |
| test/examples.lean | |
| Try this: simp only [eq_self_iff_true] | |
| cumulative profiling times: | |
| compilation 0.874ms | |
| decl post-processing 3.23ms | |
| elaboration 0.711ms | |
| elaboration: tactic compilation 197ms | |
| elaboration: tactic execution 15.5s | |
| parsing 425ms | |
| type checking 0.377ms | |
| test/expr.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 34.5ms | |
| elaboration: tactic execution 0ms | |
| test/expr_lens.lean | |
| cumulative profiling times: | |
| compilation 26.6ms | |
| decl post-processing 0.0115ms | |
| elaboration 77.3ms | |
| elaboration: tactic compilation 28.7ms | |
| elaboration: tactic execution 0ms | |
| parsing 0.918ms | |
| type checking 1.41ms | |
| test/ext.lean | |
| cumulative profiling times: | |
| compilation 0.0071ms | |
| decl post-processing 55.7ms | |
| elaboration 1.94s | |
| elaboration: tactic compilation 305ms | |
| elaboration: tactic execution 6.92s | |
| parsing 982ms | |
| type checking 0.495ms | |
| test/fin_cases.lean | |
| cumulative profiling times: | |
| compilation 0.443ms | |
| decl post-processing 1.12ms | |
| elaboration 0.162ms | |
| elaboration: tactic compilation 372ms | |
| elaboration: tactic execution 14.7s | |
| parsing 670ms | |
| type checking 0.0328ms | |
| test/finish1.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 645ms | |
| elaboration: tactic execution 3.48s | |
| parsing 1.18s | |
| test/finish2.lean | |
| cumulative profiling times: | |
| compilation 0.0019ms | |
| decl post-processing 0.0085ms | |
| elaboration 440ms | |
| elaboration: tactic compilation 1.26s | |
| elaboration: tactic execution 18.1s | |
| parsing 2.83s | |
| type checking 0.0801ms | |
| test/finish3.lean | |
| cumulative profiling times: | |
| compilation 0.0023ms | |
| decl post-processing 0.0104ms | |
| elaboration 715ms | |
| elaboration: tactic compilation 515ms | |
| elaboration: tactic execution 5.79s | |
| parsing 1s | |
| type checking 0.138ms | |
| test/finish4.lean | |
| cumulative profiling times: | |
| compilation 1.05ms | |
| decl post-processing 4.63ms | |
| elaboration 1.55s | |
| elaboration: tactic compilation 57.4ms | |
| elaboration: tactic execution 1.62s | |
| parsing 129ms | |
| type checking 0.636ms | |
| test/hint.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 292ms | |
| elaboration: tactic execution 1.3s | |
| parsing 57ms | |
| test/inhabit.lean | |
| cumulative profiling times: | |
| compilation 0.0183ms | |
| decl post-processing 2.36ms | |
| elaboration 191ms | |
| elaboration: tactic compilation 62.7ms | |
| elaboration: tactic execution 0ms | |
| parsing 81ms | |
| type checking 0.39ms | |
| test/interval_cases.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 672ms | |
| elaboration: tactic execution 30.4s | |
| parsing 1.32s | |
| test/library_search/basic.lean | |
| Try this: refine if_neg _ | |
| Try this: refine eq.symm _ | |
| Try this: refine eq_comm.mp _ | |
| Try this: refine dif_neg _ | |
| Try this: refine eq_of_heq _ | |
| Try this: refine heq_iff_eq.mp _ | |
| Try this: refine sup_eq_left.mpr _ | |
| Try this: refine max_eq_left _ | |
| Try this: refine plift.up.inj _ | |
| Try this: refine ulift.up.inj _ | |
| Try this: refine nat.succ_inj _ | |
| Try this: refine nat.bit0_inj _ | |
| Try this: refine nat.succ.inj _ | |
| Try this: refine nat.bit1_inj _ | |
| Try this: refine nat.succ_inj'.mp _ | |
| Try this: refine int.of_nat.inj _ | |
| Try this: refine int.of_nat_inj _ | |
| Try this: refine has_top.mk.inj _ | |
| Try this: refine has_one.mk.inj _ | |
| Try this: refine sup_of_le_left _ | |
| Try this: refine has_bot.mk.inj _ | |
| Try this: refine option.some_inj.mp _ | |
| Try this: refine option.some.inj _ | |
| Try this: refine int.coe_nat_inj _ | |
| Try this: refine has_zero.mk.inj _ | |
| Try this: refine congr _ _ | |
| Try this: refine let_eq _ _ | |
| Try this: refine sum.inl.inj _ | |
| Try this: refine sum.inr.inj _ | |
| Try this: refine le_antisymm _ _ | |
| Try this: refine psum.inr.inj _ | |
| Try this: refine le_antisymm' _ _ | |
| Try this: refine (add_left_inj _).mp _ | |
| Try this: refine psum.inl.inj _ | |
| Try this: refine (nat.fact_inj _).mp _ | |
| Try this: refine (divp_left_inj _).mp _ | |
| Try this: refine except.ok.inj _ | |
| Try this: refine (add_right_inj _).mp _ | |
| Try this: refine sum.inl.inj_iff.mp _ | |
| Try this: refine eq.trans _ _ | |
| Try this: refine inv_unique _ _ | |
| Try this: refine neg_unique _ _ | |
| Try this: refine char.mk.inj _ | |
| Try this: refine nat.pred_inj _ _ _ | |
| Try this: refine (eq.congr_left _).mp _ | |
| Try this: refine (eq.congr_right _).mp _ | |
| Try this: refine fin.mk.inj _ | |
| Try this: refine nat.sub_cancel _ _ _ | |
| Try this: refine subtype.mk.inj _ | |
| Try this: refine (eq.congr _ _).mp _ | |
| cumulative profiling times: | |
| compilation 6.03ms | |
| decl post-processing 2.39ms | |
| elaboration 34.9s | |
| elaboration: tactic compilation 671ms | |
| elaboration: tactic execution 197s | |
| parsing 380ms | |
| type checking 1.04ms | |
| test/library_search/ordered_ring.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 14.5ms | |
| elaboration: tactic execution 3.19s | |
| parsing 7.87ms | |
| test/library_search/ring_theory.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 47.6ms | |
| elaboration: tactic execution 100s | |
| parsing 14.8ms | |
| test/linarith.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 976ms | |
| elaboration: tactic execution 9.44s | |
| parsing 848ms | |
| test/lint.lean | |
| cumulative profiling times: | |
| compilation 17.3ms | |
| decl post-processing 9.48ms | |
| elaboration 160ms | |
| elaboration: tactic compilation 404ms | |
| elaboration: tactic execution 1.02s | |
| parsing 2.39ms | |
| type checking 2.02ms | |
| test/lint_coe_t.lean | |
| cumulative profiling times: | |
| #eval execution 0ms | |
| compilation 2.68ms | |
| decl post-processing 5.76ms | |
| elaboration 223ms | |
| elaboration: tactic compilation 38.1ms | |
| elaboration: tactic execution 166ms | |
| parsing 0.944ms | |
| type checking 1.48ms | |
| test/lint_coe_to_fun.lean | |
| cumulative profiling times: | |
| #eval execution 2ms | |
| compilation 3.7ms | |
| decl post-processing 3.58ms | |
| elaboration 2.81ms | |
| parsing 0.506ms | |
| type checking 0.385ms | |
| test/lint_simp_comm.lean | |
| cumulative profiling times: | |
| #eval execution 21ms | |
| compilation 0.0022ms | |
| decl post-processing 0.328ms | |
| elaboration 29ms | |
| elaboration: tactic compilation 24.4ms | |
| elaboration: tactic execution 40ms | |
| parsing 31.9ms | |
| type checking 0.314ms | |
| test/lint_simp_nf.lean | |
| cumulative profiling times: | |
| #eval execution 138ms | |
| compilation 1.55ms | |
| decl post-processing 2.38ms | |
| elaboration 23.4ms | |
| elaboration: tactic compilation 24.7ms | |
| elaboration: tactic execution 242ms | |
| parsing 33.9ms | |
| type checking 0.491ms | |
| test/lint_simp_var_head.lean | |
| cumulative profiling times: | |
| #eval execution 0ms | |
| elaboration: tactic compilation 33.9ms | |
| elaboration: tactic execution 228ms | |
| parsing 69.9ms | |
| test/local_cache.lean | |
| cumulative profiling times: | |
| compilation 99.5ms | |
| decl post-processing 22.9ms | |
| elaboration 3.76s | |
| elaboration: tactic compilation 723ms | |
| elaboration: tactic execution 0ms | |
| parsing 204ms | |
| type checking 8.67ms | |
| test/localized/import1.lean | |
| test/localized/import2.lean | |
| test/localized/import3.lean | |
| test/localized/localized.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 63.6ms | |
| elaboration: tactic execution 493ms | |
| parsing 90.6ms | |
| test/logic_inline.lean | |
| cumulative profiling times: | |
| #eval execution 0ms | |
| compilation 1.71ms | |
| decl post-processing 0.0087ms | |
| elaboration 0.737ms | |
| parsing 0.203ms | |
| type checking 0.0868ms | |
| test/matrix.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 53.8ms | |
| elaboration: tactic execution 14.3s | |
| parsing 99.2ms | |
| test/mk_iff_of_inductive.lean | |
| test/mllist.lean | |
| cumulative profiling times: | |
| compilation 9.56ms | |
| decl post-processing 2.54ms | |
| elaboration 72.2ms | |
| elaboration: tactic compilation 83.1ms | |
| elaboration: tactic execution 0ms | |
| parsing 0.846ms | |
| type checking 1.46ms | |
| test/monotonicity.lean | |
| cumulative profiling times: | |
| compilation 1.97ms | |
| decl post-processing 40.4ms | |
| elaboration 7.99s | |
| elaboration: tactic compilation 1.12s | |
| elaboration: tactic execution 41s | |
| parsing 3.13s | |
| type checking 2.03ms | |
| test/monotonicity/test_cases.lean | |
| cumulative profiling times: | |
| compilation 149ms | |
| decl post-processing 1.08ms | |
| elaboration 200ms | |
| elaboration: tactic compilation 118ms | |
| elaboration: tactic execution 218ms | |
| parsing 4.37ms | |
| type checking 5.24ms | |
| test/norm_cast.lean | |
| cumulative profiling times: | |
| compilation 7.56ms | |
| decl post-processing 93.6ms | |
| elaboration 848ms | |
| elaboration: tactic compilation 651ms | |
| elaboration: tactic execution 9.83s | |
| parsing 417ms | |
| type checking 3.01ms | |
| test/norm_cast_cardinal.lean | |
| cumulative profiling times: | |
| compilation 0.0029ms | |
| decl post-processing 14.9ms | |
| elaboration 69.6ms | |
| elaboration: tactic compilation 51.3ms | |
| elaboration: tactic execution 150ms | |
| parsing 27.9ms | |
| type checking 0.327ms | |
| test/norm_cast_coe_fn.lean | |
| cumulative profiling times: | |
| compilation 6.67ms | |
| decl post-processing 9.69ms | |
| elaboration 8.32ms | |
| elaboration: tactic compilation 10.2ms | |
| elaboration: tactic execution 0ms | |
| parsing 7.55ms | |
| type checking 1.41ms | |
| test/norm_cast_int.lean | |
| cumulative profiling times: | |
| #eval execution 414ms | |
| elaboration: tactic compilation 7.42ms | |
| elaboration: tactic execution 130ms | |
| parsing 5.1ms | |
| test/norm_cast_lemma_order.lean | |
| cumulative profiling times: | |
| #eval execution 395ms | |
| test/norm_cast_sum_lambda.lean | |
| cumulative profiling times: | |
| #eval execution 2ms | |
| elaboration: tactic compilation 14.5ms | |
| elaboration: tactic execution 21ms | |
| parsing 7.71ms | |
| test/norm_num.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 2.84s | |
| elaboration: tactic execution 15.3s | |
| parsing 2.65s | |
| test/nth_rewrite.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 157ms | |
| elaboration: tactic execution 80ms | |
| parsing 440ms | |
| test/omega.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 502ms | |
| elaboration: tactic execution 2.43s | |
| parsing 187ms | |
| test/packaged_goal.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 85.5ms | |
| elaboration: tactic execution 21ms | |
| parsing 9.57ms | |
| test/push_neg.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 145ms | |
| elaboration: tactic execution 71ms | |
| parsing 263ms | |
| test/rat.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 44.8ms | |
| elaboration: tactic execution 0ms | |
| test/rcases.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 238ms | |
| elaboration: tactic execution 275ms | |
| parsing 422ms | |
| test/refine_struct.lean | |
| cumulative profiling times: | |
| compilation 2.04ms | |
| decl post-processing 2.98ms | |
| elaboration 70.3ms | |
| elaboration: tactic compilation 171ms | |
| elaboration: tactic execution 19ms | |
| parsing 232ms | |
| type checking 0.221ms | |
| test/rename_var.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 59.2ms | |
| elaboration: tactic execution 0ms | |
| parsing 79.4ms | |
| test/replacer.lean | |
| cumulative profiling times: | |
| compilation 25.8ms | |
| decl post-processing 2.1ms | |
| elaboration 32.9ms | |
| elaboration: tactic compilation 79.6ms | |
| elaboration: tactic execution 0ms | |
| parsing 4.75ms | |
| type checking 1.99ms | |
| test/restate_axiom.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 39ms | |
| elaboration: tactic execution 0ms | |
| parsing 77.7ms | |
| test/rewrite.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 146ms | |
| elaboration: tactic execution 42ms | |
| parsing 276ms | |
| test/ring.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 237ms | |
| elaboration: tactic execution 38.5s | |
| parsing 323ms | |
| test/ring_exp.lean | |
| cumulative profiling times: | |
| compilation 1.07ms | |
| decl post-processing 85.6ms | |
| elaboration 3.35s | |
| elaboration: tactic compilation 705ms | |
| elaboration: tactic execution 28.1s | |
| parsing 860ms | |
| type checking 0.328ms | |
| test/simp_command.lean | |
| 0 | |
| 3 | |
| 3 | |
| 3 | |
| 3 + (3 - 3) | |
| x | |
| x | |
| x + (x - x) | |
| x + 0 | |
| λ (x : ℝ), (cos x * exp x - sin x * exp x) / exp x ^ 2 | |
| (cos x * exp x - sin x * exp x) / exp x ^ 2 | |
| 55 | |
| 1 | |
| true | |
| true | |
| true | |
| true | |
| true | |
| true | |
| cumulative profiling times: | |
| compilation 1.42ms | |
| decl post-processing 1.15ms | |
| elaboration 8.35ms | |
| elaboration: tactic compilation 27.9ms | |
| elaboration: tactic execution 12s | |
| parsing 50.1ms | |
| type checking 0.171ms | |
| test/simp_result.lean | |
| cumulative profiling times: | |
| compilation 18ms | |
| decl post-processing 0.0083ms | |
| elaboration 52.6ms | |
| elaboration: tactic compilation 1.27s | |
| elaboration: tactic execution 1.61s | |
| parsing 311ms | |
| type checking 0.78ms | |
| test/simp_rw.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 96.5ms | |
| elaboration: tactic execution 36ms | |
| parsing 129ms | |
| test/simps.lean | |
| cumulative profiling times: | |
| compilation 33.5ms | |
| decl post-processing 116ms | |
| elaboration 57.4ms | |
| elaboration: tactic compilation 334ms | |
| elaboration: tactic execution 863ms | |
| parsing 152ms | |
| type checking 5.98ms | |
| test/solve_by_elim.lean | |
| cumulative profiling times: | |
| compilation 4.02ms | |
| decl post-processing 1.24ms | |
| elaboration 86.2ms | |
| elaboration: tactic compilation 377ms | |
| elaboration: tactic execution 18ms | |
| parsing 346ms | |
| type checking 0.62ms | |
| test/split_ifs.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 66.2ms | |
| elaboration: tactic execution 148ms | |
| parsing 82.8ms | |
| test/suggest.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 316ms | |
| elaboration: tactic execution 44s | |
| parsing 86.4ms | |
| test/tactics.lean | |
| cumulative profiling times: | |
| compilation 25.6ms | |
| decl post-processing 9.24ms | |
| elaboration 111ms | |
| elaboration: tactic compilation 1.07s | |
| elaboration: tactic execution 3.19s | |
| parsing 1.66s | |
| type checking 3.61ms | |
| test/tauto.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 293ms | |
| elaboration: tactic execution 707ms | |
| parsing 147ms | |
| test/terminal_goal.lean | |
| cumulative profiling times: | |
| compilation 2.71ms | |
| decl post-processing 4.56ms | |
| elaboration 875ms | |
| elaboration: tactic compilation 146ms | |
| elaboration: tactic execution 160ms | |
| parsing 30.7ms | |
| type checking 0.785ms | |
| test/tidy.lean | |
| cumulative profiling times: | |
| compilation 10ms | |
| decl post-processing 3.93ms | |
| elaboration 920ms | |
| elaboration: tactic compilation 72.5ms | |
| elaboration: tactic execution 588ms | |
| parsing 75.2ms | |
| type checking 1.26ms | |
| test/transport/basic.lean | |
| cumulative profiling times: | |
| compilation 70.3ms | |
| decl post-processing 262ms | |
| elaboration 21.6s | |
| elaboration: tactic compilation 97.3ms | |
| elaboration: tactic execution 19.7s | |
| parsing 172ms | |
| type checking 223ms | |
| test/traversable.lean | |
| cumulative profiling times: | |
| compilation 28.2ms | |
| decl post-processing 2.7ms | |
| elaboration 45.9ms | |
| elaboration: tactic compilation 4.68ms | |
| elaboration: tactic execution 9ms | |
| parsing 0.76ms | |
| type checking 0.621ms | |
| test/trunc_cases.lean | |
| cumulative profiling times: | |
| compilation 0.657ms | |
| decl post-processing 0.809ms | |
| elaboration 35.2ms | |
| elaboration: tactic compilation 118ms | |
| elaboration: tactic execution 321ms | |
| parsing 137ms | |
| type checking 0.685ms | |
| test/where.lean | |
| cumulative profiling times: | |
| compilation 122ms | |
| decl post-processing 10.9ms | |
| elaboration 622ms | |
| elaboration: tactic compilation 82.1ms | |
| elaboration: tactic execution 0ms | |
| parsing 34ms | |
| type checking 9.63ms | |
| test/wlog.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 423ms | |
| elaboration: tactic execution 5.68s | |
| parsing 1.16s |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment