Add the ability to include line numbers within todo items or sections of the Lean code so that people can write to-dos about specific theorems or specific areas of the code. This should work nicely with the website, which would also need updating with this change. It would also be nice to have a shortcut on VS code where you can highlight a given section of text and add a to-do item with respect to that section of text.
Add the ability to include line numbers within todo items or sections of the Lean code so that people can write to-dos about specific theorems or specific areas of the code. This should work nicely with the website, which would also need updating with this change. It would also be nice to have a shortcut on VS code where you can highlight a given section of text and add a to-do item with respect to that section of text.