search

leanprover-community / mathport

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

use #align_import instead of the header comment #250

Closed eric-wieser closed 1 year ago

eric-wieser commented 1 year ago

Mathport still doesn't actually use the align_import information, but it does now generate it.