Zulip Chat Archive
Stream: lean4
Topic: Detect generation of new constants in elaboration
Leni Aniva (Jan 18 2025 at 20:15):
Sometimes elaborating match expressions or tactics can lead to the generation of new constants.
Is there an idiomatic way to detect or control this process?
Last updated: May 02 2025 at 03:31 UTC