Stream: Beginner Questions

Topic: `no_notation` causes major slowdown


view this post on Zulip Hanno Becker (Mar 07 2023 at 11:19):

Somewhat paradoxically, I am observing a major parsing slowdown after inserting a should-do-nothing no_notation ... notation ... pair in my code. How is that possible? Is no_notation not truly inverse to notation?

view this post on Zulip Hanno Becker (Mar 07 2023 at 12:42):

Adding to the confusion, the slow down is theories not even using said notation


Last updated: Dec 21 2024 at 16:20 UTC