diff --git a/doc/lean3changes.md b/doc/lean3changes.md index 73080d1fb4..cf8b217208 100644 --- a/doc/lean3changes.md +++ b/doc/lean3changes.md @@ -39,7 +39,7 @@ def Sum.str : Option Nat → String := * Implicit lambdas -In Lean 3 stdlib, we find many [instances](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39) of the dreaful `@`+`_` idiom. +In Lean 3 stdlib, we find many [instances](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39) of the dreadful `@`+`_` idiom. It is often used when we the expected type is a function type with implicit arguments, and we have a constant (`reader_t.pure` in the example) which also takes implicit arguments. In Lean 4, the elaborator automatically introduces lambda's for consuming implicit arguments. We are still exploring this feature and analyzing its impact, but the experience so far has been very positive. As an example,