Zulip Chat Archive
Stream: lean4
Topic: Editing code below `save`
Martin Dvořák (May 02 2024 at 13:53):
In some rare situations, editing code below save makes code above save throw error:
aesop: error in norm simp: elaboration interrupted
Do you also have this experience?
Last updated: May 02 2025 at 03:31 UTC