search

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 added correctly #125

Closed gebner closed 2 years ago

gebner commented 2 years ago

We get open_locale BigOperators -- unknown namespace 'BigOperators' in mathport. This is because we don't execute the localized command, but the regular notation command during synport.