Localized notation is not scoped in binport

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

43 stars 15 forks source link

Localized notation is not scoped in binport #143

Open gebner opened 2 years ago

gebner commented 2 years ago

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.