Maximilian Vollath (Oct 30 2024 at 17:01): Maximilian Vollath (Oct 30 2024 at 17:01):Hello, I like to simplify bigger definitions with a "let" statement to make them more readable. However, I noticed that this does not behave like a simple abbreviation. Rather it internally turns my function into a mess of lambda function applications which often complicates proofs. Because of this I started to use abbreviations for this purpose instead, which is uglier.
Is this just an issue with my approach or is this intetional? What is the actual use case for let statements?
Fabian Huch (Oct 30 2024 at 17:19):I don't know if this is the historic reason, but if let would be an abbreviation rather than a constant, you could not use it well for code generation
Fabian Huch (Oct 30 2024 at 17:27):But if you are too bothered, you can write your own syntax translation for an abbreviated let :shrug:
Mathias Fleury (Oct 30 2024 at 17:51):definition X where
X_internal_def: "X = (let a = 0::nat in undefined a)"
lemmas X_def = X_internal_def[unfolded Let_def]
although I am not sure why there would be a "mess of lambda function" in the proof, because you can simply use Let_def…
Mathias Fleury (Oct 30 2024 at 17:52):Also unfolding lets in general can make you term much bigger
Maximilian Vollath (Oct 31 2024 at 07:04):Thank you! I actually didn't know about just unfolding the lemma.
Last updated: Dec 21 2024 at 16:20 UTC