These #prints and surrounding comments are annoying to remove when re-porting files, and having the declarations commented out isn't particularly useful anyway.
The real motivation here is to make mathport produce a tree that is suitable for inserting between the mathlib3 and mathlib4 history, with ideally-minimal diffs
These
#prints and surrounding comments are annoying to remove when re-porting files, and having the declarations commented out isn't particularly useful anyway.The real motivation here is to make mathport produce a tree that is suitable for inserting between the mathlib3 and mathlib4 history, with ideally-minimal diffs