Compare have, let, haveI, letI #472
Description
What question should the reference manual answer?
The difference between let and have is something that most Lean users need to learn about at some point. The constructs haveI and letI are less well-known and also much less well-understood. This is made worse by the fact that haveI meant something completely different in Lean 3 (it reset the instance cache), and so some users still use haveI today in situations where they should just be using have instead. The docstrings for haveI and letI explain what sets them apart from have and let, but they do so using very low-level language (let_fun, which the reference manual's jump-to box doesn't even find), so unless you know a lot about Lean the explanation isn't really helpful.
So the questions are
- What is the difference between
have,let,haveI,letI? - When should I use which (ideally with examples)?