mathport icon indicating copy to clipboard operation
mathport copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Localized notation is not scoped in binport

Open gebner opened this issue 3 years ago • 0 comments

For example the unit interval I is global notation in the binport. This breaks the variable declaration (I : ModelWithCorners 𝕜 E H) in Geometry.Manifold.Mfderiv.

gebner avatar Apr 29 '22 19:04 gebner