doc: auto bound implicit arguments

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)

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)
+```

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 ' +