fix: use localized in synport

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

43 stars 15 forks source link

fix: use localized in synport #128

Closed digama0 closed 2 years ago

digama0 commented 2 years ago

fixes #125

gebner commented 2 years ago

This fails spectacularly, presumably because the namespace calculation in trNotationCmd is wrong: [PrettyPrinter.parenthesize.backtrack] unexpected node kind 'Algebra.BigOperators.Basic.«term∑_in_,_»', expected 'antiquot'-/-- failed to format: unknown constant 'Algebra.BigOperators.Basic.«term∑_in_,_»'