From eb11416edc06cf8cedd4750ca9d6587a2251471e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Dec 2020 16:38:55 -0800
Subject: [PATCH] doc: auto bound implicit arguments

---
 doc/SUMMARY.md   |  1 +
 doc/autobound.md | 45 +++++++++++++++++++++++++++++++++++++++++++++
 doc/highlight.js |  2 +-
 3 files changed, 47 insertions(+), 1 deletion(-)
 create mode 100644 doc/autobound.md

diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index df228bd1f8..a2f539e3ce 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -15,6 +15,7 @@
   - [Sections](./sections.md)
   - [Namespaces](./namespaces.md)
   - [Implicit Arguments](./implicit.md)
+  - [Auto Bound Implicit Arguments](./autobound.md)
 - [Functions](./functions.md)
 - [Type classes](./typeclass.md)
 - [The `do` Notation](./do.md)
diff --git a/doc/autobound.md b/doc/autobound.md
new file mode 100644
index 0000000000..51c2e3897f
--- /dev/null
+++ b/doc/autobound.md
@@ -0,0 +1,45 @@
+## Auto Bound Implict Arguments
+
+In the previous section, we have shown how implicit arguments make functions more convenient to use.
+However, functions such as `compose` are still quite verbose to define. Note that the universe
+polymorphic `compose` is even more verbose than the one previously defined.
+
+```lean
+universes u v w
+def compose {α : Type u} {β : Type v} {γ : Type w}
+            (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+```
+
+You can avoid the `universe` command by providing the universe parameters when defining `compose`.
+
+```lean
+def compose.{u, v, w}
+            {α : Type u} {β : Type v} {γ : Type w}
+            (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+```
+
+Lean 4 supports a new feature called *auto bound implicit arguments*. It makes functions such as
+`compose` much more convenient to write. When Lean processes the header of a declaration,
+any unbound identifier is automatically added as an implicit argument *if* it is a single lower case or
+greek letter. With this feature, we can write `compose` as
+
+```lean
+def compose (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+
+#check @compose
+-- {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ
+```
+Note that, Lean inferred a more general type using `Sort` instead of `Type`.
+
+Although we love this feature and use it extensively when implementing Lean,
+we realize some users may feel uncomfortable with it. Thus, you can disable it using
+the command `set_option autoBoundImplicitLocal false`.
+```lean
+set_option autoBoundImplicitLocal false
+/- The following definition produces `unknown identifier` errors -/
+-- def compose (g : β → γ) (f : α → β) (x : α) : γ :=
+--   g (f x)
+```
diff --git a/doc/highlight.js b/doc/highlight.js
index 90f6c6b8df..2c7352a60b 100644
--- a/doc/highlight.js
+++ b/doc/highlight.js
@@ -1106,7 +1106,7 @@ hljs.registerLanguage("lean", function(hljs) {
   var LEAN_KEYWORDS = {
     $pattern: /#?\w+/,
     keyword:
-      'theorem|10 def class structure instance ' +
+      'theorem|10 def class structure instance set_option ' +
       'example inductive coinductive ' +
       'axiom constant ' +
       'partial unsafe private protected ' +