Commit 2023-11-09 19:09 332340d8

View on Github →

fix: correct precedence for coercion arrows (#8297) The new precedences match coeNotation in core:

syntax:1024 (name := coeNotation) "↑" term:1024 : term

They also match the precedence in Lean 3.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/Data/DFinsupp/Basic.lean

Modified Mathlib/LinearAlgebra/Ray.lean

modified theorem sameRay_of_mem_orbit

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/Order/Hom/Basic.lean

modified theorem OrderIso.coe_dualDual

modified theorem OrderIso.coe_refl

modified theorem OrderIso.coe_trans

Modified Mathlib/Tactic/Coe.lean