Created
May 22, 2021 19:35
-
-
Save fpvandoorn/015ce16dbd42f3ec33f26f44ef031c3a to your computer and use it in GitHub Desktop.
all declarations (including automatically generated ones) that are ill-typed on commit 0e216ce00.
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
| /- Checking 74465 declarations (plus 74875 automatically generated ones) in mathlib (only in imported files) -/ | |
| /- The `check_type` linter reports: -/ | |
| /- THE STATEMENTS OF THE FOLLOWING DECLARATIONS DO NOT TYPE-CHECK. | |
| Some definitions in the statement are marked @[irreducible], which means that the statement is now ill-formed. It is likely that these definitions were locally marked @[reducible], and that type-class instances were applied that don't apply when the definitions are @[irreducible].: -/ | |
| -- algebra\category\Mon\adjunctions.lean | |
| #print adjoin_one.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print adjoin_zero_map /- The statement doesn't type-check -/ | |
| #print adjoin_zero.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print adjoin_one_map /- The statement doesn't type-check -/ | |
| #print adjoin_zero_adj.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print adjoin_one_adj._proof_2 /- The statement doesn't type-check -/ | |
| #print adjoin_one_adj.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print adjoin_zero_adj._proof_1 /- The statement doesn't type-check -/ | |
| #print adjoin_zero_adj._proof_2 /- The statement doesn't type-check -/ | |
| #print adjoin_one_adj._proof_1 /- The statement doesn't type-check -/ | |
| -- algebra\group\with_one.lean | |
| #print with_one.monad.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.monad.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_one.has_one.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.has_zero.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.nontrivial.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_one.nontrivial.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.has_coe_t.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_one.has_coe_t.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_one.mul_one_class.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.add_zero_class.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_one.monoid.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.add_monoid.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_one.comm_monoid.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.add_comm_monoid.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.coe_add_hom_apply /- The statement doesn't type-check -/ | |
| #print with_one.coe_mul_hom_apply /- The statement doesn't type-check -/ | |
| #print with_one.lift._proof_3 /- The statement doesn't type-check -/ | |
| #print with_zero.lift._proof_3 /- The statement doesn't type-check -/ | |
| #print with_one.lift._proof_1 /- The statement doesn't type-check -/ | |
| #print with_one.lift._proof_4 /- The statement doesn't type-check -/ | |
| #print with_zero.lift.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.lift._proof_2 /- The statement doesn't type-check -/ | |
| #print with_one.lift.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.lift._proof_4 /- The statement doesn't type-check -/ | |
| #print with_zero.lift._proof_1 /- The statement doesn't type-check -/ | |
| #print with_one.lift._proof_2 /- The statement doesn't type-check -/ | |
| #print with_zero.mul_zero_class._proof_2 /- The statement doesn't type-check -/ | |
| #print with_zero.mul_zero_class._proof_1 /- The statement doesn't type-check -/ | |
| #print with_zero.mul_zero_class.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.semigroup_with_zero._match_1.equations._eqn_2 /- The statement doesn't type-check -/ | |
| #print with_zero.semigroup_with_zero._match_1.equations._eqn_3 /- The statement doesn't type-check -/ | |
| #print with_zero.semigroup_with_zero._match_1.equations._eqn_4 /- The statement doesn't type-check -/ | |
| #print with_zero.semigroup_with_zero._match_1.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.comm_semigroup._match_1.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.comm_semigroup._match_1.equations._eqn_2 /- The statement doesn't type-check -/ | |
| #print with_zero.comm_semigroup._match_1.equations._eqn_3 /- The statement doesn't type-check -/ | |
| #print with_zero.mul_zero_one_class._match_2.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.mul_zero_one_class._match_1.equations._eqn_2 /- The statement doesn't type-check -/ | |
| #print with_zero.mul_zero_one_class._match_1.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.mul_zero_one_class._match_2.equations._eqn_2 /- The statement doesn't type-check -/ | |
| -- algebra\homology\homological_complex.lean | |
| #print chain_complex.mk_aux.equations._eqn_2 /- The statement doesn't type-check -/ | |
| #print chain_complex.mk_hom_aux.equations._eqn_2 /- The statement doesn't type-check -/ | |
| #print cochain_complex.mk_aux.equations._eqn_2 /- The statement doesn't type-check -/ | |
| #print cochain_complex.mk_hom_aux.equations._eqn_2 /- The statement doesn't type-check -/ | |
| -- algebra\homology\homotopy.lean | |
| #print homotopy.mk_inductive_aux₁.equations._eqn_3 /- The statement doesn't type-check -/ | |
| -- algebra\ordered_monoid.lean | |
| #print with_zero.preorder.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.partial_order.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.order_bot.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.lattice.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.linear_order.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_top.add_semigroup.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_top.add_comm_semigroup.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_top.add_monoid.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_top.add_comm_monoid.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_zero.canonically_ordered_add_monoid._proof_13 /- The statement doesn't type-check -/ | |
| #print with_zero.canonically_ordered_add_monoid._match_1 /- The statement doesn't type-check -/ | |
| #print with_zero.canonically_ordered_add_monoid._match_1.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print with_top.canonically_ordered_add_monoid._match_1.equations._eqn_4 /- The statement doesn't type-check -/ | |
| -- algebra\ring_quot.lean | |
| #print ring_quot.mk_alg_hom.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- algebraic_topology\simplex_category.lean | |
| #print simplex_category.mk.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print simplex_category.len.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print simplex_category.hom.mk.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print simplex_category.hom.to_preorder_hom.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- category_theory\monoidal\free\coherence.lean | |
| #print category_theory.free_monoidal_category.normalize_map_aux.equations._eqn_9 /- The statement doesn't type-check -/ | |
| -- category_theory\monoidal\opposite.lean | |
| #print category_theory.monoidal_opposite.mop.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print category_theory.monoidal_opposite.unmop.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- category_theory\opposites.lean | |
| #print category_theory.nat_trans.op_app /- The statement doesn't type-check -/ | |
| #print category_theory.nat_trans.remove_left_op_app /- The statement doesn't type-check -/ | |
| #print category_theory.nat_trans.right_op_app /- The statement doesn't type-check -/ | |
| -- combinatorics\quiver.lean | |
| #print quiver.hom.op.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print quiver.hom.unop.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- data\opposite.lean | |
| #print opposite.op.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print opposite.unop.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- data\rat\order.lean | |
| #print rat.decidable_le.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print rat.decidable_le._main.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print rat.linear_order.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- group_theory\perm\sign.lean | |
| #print equiv.perm.swap_factors_aux.equations._eqn_2 /- The statement doesn't type-check -/ | |
| -- linear_algebra\clifford_algebra\basic.lean | |
| #print clifford_algebra.ι.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print clifford_algebra.lift._proof_4 /- The statement doesn't type-check -/ | |
| #print clifford_algebra.lift.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print clifford_algebra.lift._proof_3 /- The statement doesn't type-check -/ | |
| -- ring_theory\fractional_ideal.lean | |
| #print ring.fractional_ideal.comm_semiring._proof_20 /- The statement doesn't type-check -/ | |
| #print ring.fractional_ideal.is_principal.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- ring_theory\valuation\basic.lean | |
| #print add_valuation.has_coe_to_fun.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print add_valuation.of.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print add_valuation.comap.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print add_valuation.map.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print add_valuation.is_equiv.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print add_valuation.supp.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print add_valuation.on_quot_val.equations._eqn_1 /- The statement doesn't type-check -/ | |
| #print add_valuation.on_quot.equations._eqn_1 /- The statement doesn't type-check -/ | |
| -- set_theory\zfc.lean | |
| #print pSet.resp.eval_aux.equations._eqn_2 /- The statement doesn't type-check -/ | |
| #print classical.all_definable.equations._eqn_2 /- The statement doesn't type-check -/ | |
| -- tactic\linarith\datatypes.lean | |
| #print linarith.linarith_config.mk.inj_arrow /- The statement doesn't type-check -/ | |
| #print linarith.linarith_config.mk.inj_eq /- The statement doesn't type-check -/ | |
| #print linarith.linarith_config.mk.inj /- The statement doesn't type-check -/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment