feat: describe type classes (#127)

Describe type classes.

Fixes #60, #61, #62, #63, #64, and #65

Manual/Elaboration.lean

@@ -235,9 +235,8 @@ def third_of_five : List α → Option α
   | _ => none
 set_option pp.match false
 /--
-info: third_of_five.eq_def.{u_1} {α : Type u_1} :
-  ∀ (x : List α),
-    third_of_five x = third_of_five.match_1 (fun x => Option α) x (fun head head x head head => some x) fun x => none
+info: third_of_five.eq_def.{u_1} {α : Type u_1} (x✝ : List α) :
+  third_of_five x✝ = third_of_five.match_1 (fun x => Option α) x✝ (fun head head x head head => some x) fun x => none
 -/
 #guard_msgs in
 #check third_of_five.eq_def

Manual/Language.lean

@@ -7,6 +7,7 @@ Author: David Thrane Christiansen
 import VersoManual
 
 import Manual.Meta
+import Manual.Language.Classes
 import Manual.Language.Functions
 import Manual.Language.Files
 import Manual.Language.InductiveTypes
@@ -569,6 +570,7 @@ The following commands in Lean are definition-like: {TODO}[Render commands as th
 
 All of these commands cause Lean to {tech key:="elaborator"}[elaborate] a term based on a signature.
 With the exception of {syntaxKind}`example`, which discards the result, the resulting expression in Lean's core language is saved for future use in the environment.
+The {keywordOf Lean.Parser.Command.declaration}`instance` command is described in the {ref "instance-declarations"}[section on instance declarations].
 
 :::syntax Lean.Parser.Command.declaration
 ```grammar
@@ -626,26 +628,6 @@ abbrev $_ $_ where
 :::
 
 
-:::TODO
-Move `instance` to type classes section with a backreference from here
-:::
-
-:::syntax Lean.Parser.Command.instance
-```grammar
-instance $_? : $_ := $_
-```
-
-```grammar
-instance $_? : $_
-  $[| $_ => $_]*
-```
-
-```grammar
-instance $_? : $_ where
-  $_*
-```
-:::
-
 
 :::syntax Lean.Parser.Command.example
 ```grammar
@@ -774,7 +756,7 @@ This section will describe the translation of {deftech}[well-founded recursion].
 ## Controlling Reduction
 
 :::planned 58
-This section will describe {deftech}[reducible], {deftech}[semireducible], and {deftech}[irreducible] definitions.
+This section will describe {deftech}_reducibility_: {deftech}[reducible], {deftech}[semireducible], and {deftech}[irreducible] definitions.
 :::
 
 ## Partial and Unsafe Recursive Definitions
@@ -792,51 +774,14 @@ This section will describe `partial` and `unsafe` definitions:
 
 :::
 
-# Type Classes
-
-:::planned 61
-
-This introduction will describe the overall feature.
-
-:::
-
-## Class Declarations
+{include 0 Manual.Language.Classes}
 
-::: planned 60
-This section will describe the syntax of `class` and `class inductive` declarations.
-The desugaring of `class` to `structure` and thus `inductive` will be addressed, along with the determining of implicitness of method parameters. `outParam` and `semiOutParam` will also be described.
-:::
+# Dynamic Typing
 
-## Instance Declarations
-
-::: planned 62
-This section will describe the syntax of `instance` declarations, priorities, and names.
-:::
+{docstring TypeName}
 
+{docstring Dynamic}
 
-## Instance Synthesis
-%%%
-tag := "instance-synth"
-%%%
-
-::: planned 63
-This section will specify the instance synthesis algorithm.
-:::
+{docstring Dynamic.mk}
 
-## Deriving Instances
-%%%
-tag := "deriving-instances"
-%%%
-
-::: planned 64
-This section will specify syntax of `deriving` clauses and list the valid places where they may occur.
-It will also describe `deriving instance`.
-It will list the deriving handlers that ship with Lean by default.
-:::
-
-
-### Deriving Handlers
-
-::: planned 65
-This section will describe deriving handlers and how they are invoked.
-:::
+{docstring Dynamic.get?}