From c7ebc33f979dba4c39ec5875a754dc044c8c1048 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Nov 2020 11:43:57 -0800 Subject: [PATCH] chore: fix typo --- doc/lean3changes.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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,