leanprover-community / mathport

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

feat: add `redundantAlign` option #200

Closed digama0 closed 1 year ago

digama0 commented 1 year ago

This implements the option discussed in yesterday's mathport meeting. When the redundantAlign config option is set to true (the default), mathport will add a "redundant" #align line after every declaration, as a base for modification for when you actually do want an #align.

cc: @semorrison @pechersky @gebner