leanprover-community / mathport

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

Aligning `_root_.theorem_name` #204

Closed winstonyin closed 1 year ago

winstonyin commented 1 year ago
namespace my_namespace

theorem _root_.my_theorem : sorry := sorry
#align my_namespace._root_.my_theorem my_namespace._root_.my_theorem -- mathport behaviour
-- #align my_theorem my_theorem -- expected behaviour

end my_namespace

Probably something to do with this