search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.36k stars 303 forks source link

notation3 doesn't work with scoped #5343

Open Ruben-VandeVelde opened 1 year ago

alexjbest commented 1 year ago

Is this now fixed (especially after https://github.com/leanprover-community/mathlib4/pull/6793)?