You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The [refl] tag applies to refl theorems or definitions only if the instance arguments of the associated structure are ordered in a specific way, apparently, see also this Zulip thread. MWE testing some combinations:
import Mathlib.Algebra.Group.Opposite
import Mathlib.Algebra.Hom.Ring
structureRingEquiv0 (R S : Type _) [Mul R] [Mul S] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S
structureRingEquiv1 (R S : Type _) [Mul S] [Mul R] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S
structureRingEquiv2 (R S : Type _) [Mul R] [Mul S] [Add S] [Add R] extends R ≃ S, R ≃* S, R ≃+ S
structureRingEquiv3 (R S : Type _) [Mul R] [Add R] [Mul S] [Add S] extends R ≃ S, R ≃* S, R ≃+ S
structureRingEquiv4 (R S : Type _) [Mul R] [Add S] [Mul S] [Add R] extends R ≃ S, R ≃* S, R ≃+ S
@[refl]-- worksdefRingEquiv0.refl [Mul α] [Add α] : RingEquiv0 α α := sorry@[refl]-- worksdefRingEquiv1.refl [Mul α] [Add α] : RingEquiv1 α α := sorry@[refl]-- worksdefRingEquiv2.refl [Mul α] [Add α] : RingEquiv2 α α := sorry@[refl]/- @[refl] attribute only applies to lemmas proving x ∼ x, got {α : Type u_1} → [inst : Mul α] → [inst_1 : Add α] → RingEquiv3 α α -/defRingEquiv3.refl [Mul α] [Add α] : RingEquiv3 α α := sorry@[refl]/- @[refl] attribute only applies to lemmas proving x ∼ x, got {α : Type u_1} → [inst : Mul α] → [inst_1 : Add α] → RingEquiv4 α α -/defRingEquiv4.refl [Mul α] [Add α] : RingEquiv4 α α := sorry
The text was updated successfully, but these errors were encountered:
The [refl] tag applies to
refl
theorems or definitions only if the instance arguments of the associated structure are ordered in a specific way, apparently, see also this Zulip thread. MWE testing some combinations:The text was updated successfully, but these errors were encountered: