trace output for add_group (ℤ × ℤ × ℤ × ℤ)

trace.txt

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : add_group (ℤ × ℤ × ℤ × ℤ) := @prod.add_group ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] (1) ?x_3 : add_group ℤ := @prod.add_group ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @pi.add_group ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @subtype.add_group ?x_12 ?x_13 ?x_14 ?x_15
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @additive.add_group ?x_16 ?x_17
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @add_comm_group.to_add_group ?x_18 ?x_19
[class_instances] (2) ?x_19 : add_comm_group ℤ := @prod.add_comm_group ?x_20 ?x_21 ?x_22 ?x_23
failed is_def_eq
[class_instances] (2) ?x_19 : add_comm_group ℤ := @pi.add_comm_group ?x_24 ?x_25 ?x_26
failed is_def_eq
[class_instances] (2) ?x_19 : add_comm_group ℤ := @submodule.add_comm_group ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32
failed is_def_eq
[class_instances] (2) ?x_19 : add_comm_group ℤ := @nonneg_comm_group.to_add_comm_group ?x_33 ?x_34
[class_instances] (3) ?x_34 : nonneg_comm_group ℤ := @linear_nonneg_ring.to_nonneg_comm_group ?x_35 ?x_36
[class_instances] (3) ?x_34 : nonneg_comm_group ℤ := @nonneg_ring.to_nonneg_comm_group ?x_35 ?x_36
[class_instances] (4) ?x_36 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_37 ?x_38
[class_instances] (2) ?x_19 : add_comm_group ℤ := @additive.add_comm_group ?x_20 ?x_21
failed is_def_eq
[class_instances] (2) ?x_19 : add_comm_group ℤ := @ring.to_add_comm_group ?x_22 ?x_23
[class_instances] (3) ?x_23 : ring ℤ := @prod.ring ?x_24 ?x_25 ?x_26 ?x_27
failed is_def_eq
[class_instances] (3) ?x_23 : ring ℤ := @pi.ring ?x_28 ?x_29 ?x_30
failed is_def_eq
[class_instances] (3) ?x_23 : ring ℤ := @nonneg_ring.to_ring ?x_31 ?x_32
[class_instances] (4) ?x_32 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_33 ?x_34
[class_instances] (3) ?x_23 : ring ℤ := @domain.to_ring ?x_24 ?x_25
[class_instances] (4) ?x_25 : domain ℤ := @division_ring.to_domain ?x_26 ?x_27
[class_instances] (5) ?x_27 : division_ring ℤ := @field.to_division_ring ?x_28 ?x_29
[class_instances] (6) ?x_29 : field ℤ := @linear_ordered_field.to_field ?x_30 ?x_31
[class_instances] (7) ?x_31 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_32 ?x_33
[class_instances] (6) ?x_29 : field ℤ := @discrete_field.to_field ?x_30 ?x_31
[class_instances] (7) ?x_31 : discrete_field ℤ := @discrete_linear_ordered_field.to_discrete_field ?x_32 ?x_33
[class_instances] (4) ?x_25 : domain ℤ := @linear_nonneg_ring.to_domain ?x_26 ?x_27
[class_instances] (4) ?x_25 : domain ℤ := @to_domain ?x_26 ?x_27
[class_instances] (5) ?x_27 : linear_ordered_ring ℤ := @linear_nonneg_ring.to_linear_ordered_ring ?x_28 ?x_29
[class_instances] (5) ?x_27 : linear_ordered_ring ℤ := @linear_ordered_field.to_linear_ordered_ring ?x_28 ?x_29
[class_instances] (6) ?x_29 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_30 ?x_31
[class_instances] (5) ?x_27 : linear_ordered_ring ℤ := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_28 ?x_29
[class_instances] (6) ?x_29 : linear_ordered_comm_ring ℤ := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_30 ?x_31
[class_instances] (7) ?x_31 : decidable_linear_ordered_comm_ring ℤ := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_32 ?x_33 ?x_34 ?x_35
[class_instances] (7) ?x_31 : decidable_linear_ordered_comm_ring ℤ := int.decidable_linear_ordered_comm_ring
[class_instances] (1) ?x_4 : add_group (ℤ × ℤ × ℤ) := @prod.add_group ?x_32 ?x_33 ?x_34 ?x_35
[class_instances] (2) ?x_34 : add_group ℤ := @prod.add_group ?x_36 ?x_37 ?x_38 ?x_39
failed is_def_eq
[class_instances] (2) ?x_34 : add_group ℤ := @pi.add_group ?x_40 ?x_41 ?x_42
failed is_def_eq
[class_instances] (2) ?x_34 : add_group ℤ := @subtype.add_group ?x_43 ?x_44 ?x_45 ?x_46
failed is_def_eq
[class_instances] (2) ?x_34 : add_group ℤ := @additive.add_group ?x_47 ?x_48
failed is_def_eq
[class_instances] (2) ?x_34 : add_group ℤ := @add_comm_group.to_add_group ?x_49 ?x_50
[class_instances] (3) ?x_50 : add_comm_group ℤ := @prod.add_comm_group ?x_51 ?x_52 ?x_53 ?x_54
failed is_def_eq
[class_instances] (3) ?x_50 : add_comm_group ℤ := @pi.add_comm_group ?x_55 ?x_56 ?x_57
failed is_def_eq
[class_instances] (3) ?x_50 : add_comm_group ℤ := @submodule.add_comm_group ?x_58 ?x_59 ?x_60 ?x_61 ?x_62 ?x_63
failed is_def_eq
[class_instances] (3) ?x_50 : add_comm_group ℤ := @nonneg_comm_group.to_add_comm_group ?x_64 ?x_65
[class_instances] (4) ?x_65 : nonneg_comm_group ℤ := @linear_nonneg_ring.to_nonneg_comm_group ?x_66 ?x_67
[class_instances] (4) ?x_65 : nonneg_comm_group ℤ := @nonneg_ring.to_nonneg_comm_group ?x_66 ?x_67
[class_instances] (5) ?x_67 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_68 ?x_69
[class_instances] (3) ?x_50 : add_comm_group ℤ := @additive.add_comm_group ?x_51 ?x_52
failed is_def_eq
[class_instances] (3) ?x_50 : add_comm_group ℤ := @ring.to_add_comm_group ?x_53 ?x_54
[class_instances] (4) ?x_54 : ring ℤ := @prod.ring ?x_55 ?x_56 ?x_57 ?x_58
failed is_def_eq
[class_instances] (4) ?x_54 : ring ℤ := @pi.ring ?x_59 ?x_60 ?x_61
failed is_def_eq
[class_instances] (4) ?x_54 : ring ℤ := @nonneg_ring.to_ring ?x_62 ?x_63
[class_instances] (5) ?x_63 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_64 ?x_65
[class_instances] (4) ?x_54 : ring ℤ := @domain.to_ring ?x_55 ?x_56
[class_instances] (5) ?x_56 : domain ℤ := @division_ring.to_domain ?x_57 ?x_58
[class_instances] (6) ?x_58 : division_ring ℤ := @field.to_division_ring ?x_59 ?x_60
[class_instances] (7) ?x_60 : field ℤ := @linear_ordered_field.to_field ?x_61 ?x_62
[class_instances] (8) ?x_62 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_63 ?x_64
[class_instances] (7) ?x_60 : field ℤ := @discrete_field.to_field ?x_61 ?x_62
[class_instances] (8) ?x_62 : discrete_field ℤ := @discrete_linear_ordered_field.to_discrete_field ?x_63 ?x_64
[class_instances] (5) ?x_56 : domain ℤ := @linear_nonneg_ring.to_domain ?x_57 ?x_58
[class_instances] (5) ?x_56 : domain ℤ := @to_domain ?x_57 ?x_58
[class_instances] (6) ?x_58 : linear_ordered_ring ℤ := @linear_nonneg_ring.to_linear_ordered_ring ?x_59 ?x_60
[class_instances] (6) ?x_58 : linear_ordered_ring ℤ := @linear_ordered_field.to_linear_ordered_ring ?x_59 ?x_60
[class_instances] (7) ?x_60 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_61 ?x_62
[class_instances] (6) ?x_58 : linear_ordered_ring ℤ := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_59 ?x_60
[class_instances] (7) ?x_60 : linear_ordered_comm_ring ℤ := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_61 ?x_62
[class_instances] (8) ?x_62 : decidable_linear_ordered_comm_ring ℤ := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_63 ?x_64 ?x_65 ?x_66
[class_instances] (8) ?x_62 : decidable_linear_ordered_comm_ring ℤ := int.decidable_linear_ordered_comm_ring
[class_instances] (2) ?x_35 : add_group (ℤ × ℤ) := @prod.add_group ?x_63 ?x_64 ?x_65 ?x_66
[class_instances] (3) ?x_65 : add_group ℤ := @prod.add_group ?x_67 ?x_68 ?x_69 ?x_70
failed is_def_eq
[class_instances] (3) ?x_65 : add_group ℤ := @pi.add_group ?x_71 ?x_72 ?x_73
failed is_def_eq
[class_instances] (3) ?x_65 : add_group ℤ := @subtype.add_group ?x_74 ?x_75 ?x_76 ?x_77
failed is_def_eq
[class_instances] (3) ?x_65 : add_group ℤ := @additive.add_group ?x_78 ?x_79
failed is_def_eq
[class_instances] (3) ?x_65 : add_group ℤ := @add_comm_group.to_add_group ?x_80 ?x_81
[class_instances] (4) ?x_81 : add_comm_group ℤ := @prod.add_comm_group ?x_82 ?x_83 ?x_84 ?x_85
failed is_def_eq
[class_instances] (4) ?x_81 : add_comm_group ℤ := @pi.add_comm_group ?x_86 ?x_87 ?x_88
failed is_def_eq
[class_instances] (4) ?x_81 : add_comm_group ℤ := @submodule.add_comm_group ?x_89 ?x_90 ?x_91 ?x_92 ?x_93 ?x_94
failed is_def_eq
[class_instances] (4) ?x_81 : add_comm_group ℤ := @nonneg_comm_group.to_add_comm_group ?x_95 ?x_96
[class_instances] (5) ?x_96 : nonneg_comm_group ℤ := @linear_nonneg_ring.to_nonneg_comm_group ?x_97 ?x_98
[class_instances] (5) ?x_96 : nonneg_comm_group ℤ := @nonneg_ring.to_nonneg_comm_group ?x_97 ?x_98
[class_instances] (6) ?x_98 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_99 ?x_100
[class_instances] (4) ?x_81 : add_comm_group ℤ := @additive.add_comm_group ?x_82 ?x_83
failed is_def_eq
[class_instances] (4) ?x_81 : add_comm_group ℤ := @ring.to_add_comm_group ?x_84 ?x_85
[class_instances] (5) ?x_85 : ring ℤ := @prod.ring ?x_86 ?x_87 ?x_88 ?x_89
failed is_def_eq
[class_instances] (5) ?x_85 : ring ℤ := @pi.ring ?x_90 ?x_91 ?x_92
failed is_def_eq
[class_instances] (5) ?x_85 : ring ℤ := @nonneg_ring.to_ring ?x_93 ?x_94
[class_instances] (6) ?x_94 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_95 ?x_96
[class_instances] (5) ?x_85 : ring ℤ := @domain.to_ring ?x_86 ?x_87
[class_instances] (6) ?x_87 : domain ℤ := @division_ring.to_domain ?x_88 ?x_89
[class_instances] (7) ?x_89 : division_ring ℤ := @field.to_division_ring ?x_90 ?x_91
[class_instances] (8) ?x_91 : field ℤ := @linear_ordered_field.to_field ?x_92 ?x_93
[class_instances] (9) ?x_93 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_94 ?x_95
[class_instances] (8) ?x_91 : field ℤ := @discrete_field.to_field ?x_92 ?x_93
[class_instances] (9) ?x_93 : discrete_field ℤ := @discrete_linear_ordered_field.to_discrete_field ?x_94 ?x_95
[class_instances] (6) ?x_87 : domain ℤ := @linear_nonneg_ring.to_domain ?x_88 ?x_89
[class_instances] (6) ?x_87 : domain ℤ := @to_domain ?x_88 ?x_89
[class_instances] (7) ?x_89 : linear_ordered_ring ℤ := @linear_nonneg_ring.to_linear_ordered_ring ?x_90 ?x_91
[class_instances] (7) ?x_89 : linear_ordered_ring ℤ := @linear_ordered_field.to_linear_ordered_ring ?x_90 ?x_91
[class_instances] (8) ?x_91 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_92 ?x_93
[class_instances] (7) ?x_89 : linear_ordered_ring ℤ := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_90 ?x_91
[class_instances] (8) ?x_91 : linear_ordered_comm_ring ℤ := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_92 ?x_93
[class_instances] (9) ?x_93 : decidable_linear_ordered_comm_ring ℤ := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_94 ?x_95 ?x_96 ?x_97
[class_instances] (9) ?x_93 : decidable_linear_ordered_comm_ring ℤ := int.decidable_linear_ordered_comm_ring
[class_instances] (3) ?x_66 : add_group ℤ := @prod.add_group ?x_94 ?x_95 ?x_96 ?x_97
failed is_def_eq
[class_instances] (3) ?x_66 : add_group ℤ := @pi.add_group ?x_98 ?x_99 ?x_100
failed is_def_eq
[class_instances] (3) ?x_66 : add_group ℤ := @subtype.add_group ?x_101 ?x_102 ?x_103 ?x_104
failed is_def_eq
[class_instances] (3) ?x_66 : add_group ℤ := @additive.add_group ?x_105 ?x_106
failed is_def_eq
[class_instances] (3) ?x_66 : add_group ℤ := @add_comm_group.to_add_group ?x_107 ?x_108
[class_instances] (4) ?x_108 : add_comm_group ℤ := @prod.add_comm_group ?x_109 ?x_110 ?x_111 ?x_112
failed is_def_eq
[class_instances] (4) ?x_108 : add_comm_group ℤ := @pi.add_comm_group ?x_113 ?x_114 ?x_115
failed is_def_eq
[class_instances] (4) ?x_108 : add_comm_group ℤ := @submodule.add_comm_group ?x_116 ?x_117 ?x_118 ?x_119 ?x_120 ?x_121
failed is_def_eq
[class_instances] (4) ?x_108 : add_comm_group ℤ := @nonneg_comm_group.to_add_comm_group ?x_122 ?x_123
[class_instances] (5) ?x_123 : nonneg_comm_group ℤ := @linear_nonneg_ring.to_nonneg_comm_group ?x_124 ?x_125
[class_instances] (5) ?x_123 : nonneg_comm_group ℤ := @nonneg_ring.to_nonneg_comm_group ?x_124 ?x_125
[class_instances] (6) ?x_125 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_126 ?x_127
[class_instances] (4) ?x_108 : add_comm_group ℤ := @additive.add_comm_group ?x_109 ?x_110
failed is_def_eq
[class_instances] (4) ?x_108 : add_comm_group ℤ := @ring.to_add_comm_group ?x_111 ?x_112
[class_instances] (5) ?x_112 : ring ℤ := @prod.ring ?x_113 ?x_114 ?x_115 ?x_116
failed is_def_eq
[class_instances] (5) ?x_112 : ring ℤ := @pi.ring ?x_117 ?x_118 ?x_119
failed is_def_eq
[class_instances] (5) ?x_112 : ring ℤ := @nonneg_ring.to_ring ?x_120 ?x_121
[class_instances] (6) ?x_121 : nonneg_ring ℤ := @linear_nonneg_ring.to_nonneg_ring ?x_122 ?x_123
[class_instances] (5) ?x_112 : ring ℤ := @domain.to_ring ?x_113 ?x_114
[class_instances] (6) ?x_114 : domain ℤ := @division_ring.to_domain ?x_115 ?x_116
[class_instances] (7) ?x_116 : division_ring ℤ := @field.to_division_ring ?x_117 ?x_118
[class_instances] (8) ?x_118 : field ℤ := @linear_ordered_field.to_field ?x_119 ?x_120
[class_instances] (9) ?x_120 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_121 ?x_122
[class_instances] (8) ?x_118 : field ℤ := @discrete_field.to_field ?x_119 ?x_120
[class_instances] (9) ?x_120 : discrete_field ℤ := @discrete_linear_ordered_field.to_discrete_field ?x_121 ?x_122
[class_instances] (6) ?x_114 : domain ℤ := @linear_nonneg_ring.to_domain ?x_115 ?x_116
[class_instances] (6) ?x_114 : domain ℤ := @to_domain ?x_115 ?x_116
[class_instances] (7) ?x_116 : linear_ordered_ring ℤ := @linear_nonneg_ring.to_linear_ordered_ring ?x_117 ?x_118
[class_instances] (7) ?x_116 : linear_ordered_ring ℤ := @linear_ordered_field.to_linear_ordered_ring ?x_117 ?x_118
[class_instances] (8) ?x_118 : linear_ordered_field ℤ := @discrete_linear_ordered_field.to_linear_ordered_field ?x_119 ?x_120
[class_instances] (7) ?x_116 : linear_ordered_ring ℤ := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_117 ?x_118
[class_instances] (8) ?x_118 : linear_ordered_comm_ring ℤ := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_119 ?x_120
[class_instances] (9) ?x_120 : decidable_linear_ordered_comm_ring ℤ := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_121 ?x_122 ?x_123 ?x_124
[class_instances] (9) ?x_120 : decidable_linear_ordered_comm_ring ℤ := int.decidable_linear_ordered_comm_ring