Commit 2022-11-20 21:15 cd40c744

feat: #noalign command; align.precheck option (#663)

• The #noalign command is like #align but it doesn't take a lean 4 name. The semantics are that mathport will delete the theorem which would have been translated at this point, and future references will use sorry instead. I am unsure how much we will need this, but it is good for documenting intentional deletions.
• The #align command now checks that the lean 4 declaration (after stripping ₓ) exists. It still requires that the lean 4 name be fully qualified, but it will tell you if you tried to reference something that was in scope. (I don't want it to do name resolution on its own because this will make it harder to compare with the lean 3 version.) You can disable the check using set_option align.precheck false.
• The mk_iff command now does name resolution and attaches proper definition info to the input span.
• As expected, the precheck caught a ton of naming bugs in ported files.