Commit 2022-07-18 14:13 9a76952e

feat: haveI and letI syntax (#305) haveI := inst; val simulates the by haveI := inst; exact val syntax from Lean 3. While the Lean 4 have always introduces a local instance, it creates a let_fun term even when in tactic mode. The Lean 3 have tactic however inlined the value. The new haveI and letI syntax always inlines the value. See https://github.com/leanprover/lean4/issues/1313