leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

remove ₓ #170

Closed gebner closed 2 years ago

gebner commented 2 years ago

Binport should still use ₓ to disambiguate definitions. But synport should remove the ₓ when producing the Lean 4 AST.