search

leanprover-community / mathport

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

chore: output #align statements on one line #218

Closed jcommelin closed 1 year ago

rwbarton commented 1 year ago

This seems to be leaving a backtick before each name in an #align statement.