better example flow

CONTRIBUTING.md

@@ -18,9 +18,40 @@ Please remember to get in touch ahead of time to plan a larger contribution. In
  * Empirical claims about Lean should be tested, either via examples or hidden test cases.
  * Examples should be clearly marked as such, separating the description of the system from the illustrative examples.
  * Technical terms should be introduced using the `deftech` role and referred to using the `tech` role.
- * Write in US English, deferring to the Chicago Manual of Style when in doubt. Exceptions to this style may be added and documented.
+ * Write in US English, deferring to the Chicago Manual of Style 18 (CMS) when in doubt. Exceptions to this style may be added and documented.
  * One sentence per line, to make diffs easier to follow.
 
+### Style
+
+Headings should be set in title case, rather than just capitalizing the first word. This is defined in CMS rule 8.160, but a good first approximation is to capitalize the first and last words, plus all words other than the following:
+ * prepositions less than five letters when not used as adverbs or adjectives
+ * "a", "an", "the", "to" (infinitive marker), "and", "but", "for", "or", "nor"
+ * conventionally lower-case components of names, like "de" or "van"
+
+Numbered or bulleted lists should be introduced by a grammatically-complete sentence that is terminated with a colon, follow one of two options:
+
+ * All list items contain one or more complete sentences that start with a capital letter and are punctuated accordingly.
+
+ * All list items contain noun phrases or sentence fragments that begin with a lower-case letter and do not end with punctuation.
+
+That is to say, lists may consist of:
+
+ 1. complete sentences, punctuated accordingly
+
+ 2. non-sentences, punctuated accordingly
+
+In Verso, the list and the sentence with the colon should be grouped with the `paragraph` directive.
+
+
+If necessary for emphasis, a sentence that contains a list may be broken up into a vertical list element (cf Chicago rule 6.142). In this case, punctuate the list items as though they were inline in the sentence, without using a colon at the start. When using this style in this document, rememember to
+
+ * use the `paragraph` directive so the list is typeset together with its sentence,
+ * punctuate with semicolons if the list items themselves contain commas, and
+ * remember the trailing "and" and period in the penultimate and final items.
+
+
+Automated tooling is not yet capable of implementing these rules perfectly, so pull requests that bring text into compliance with this guide are very welcome.
+
 ## Markup
 
 The reference manual is written in Verso's manual genre.

Manual/Coercions.lean

@@ -53,25 +53,30 @@ The set of coercions can be extended by adding further instances of the appropri
 end
 ```
 
+:::example "Coercions"
 
-```lean (show := false) (keep := false)
--- Test the coercions in the list
+All of the following examples rely on coercions:
+
+```lean
 example (n : Nat) : Int := n
-example (n : Lean.TSyntax `ident) : Lean.TSyntax `term := n
 example (n : Fin k) : Nat := n
 example (x : α) : Option α := x
-def th (x : α) : Thunk α := x
 
-/--
-info: def th.{u_1} : {α : Type u_1} → α → Thunk α :=
-fun {α} x => { fn := fun x_1 => x }
--/
-#guard_msgs in
+def th (f : Int → String) (x : Nat) : Thunk String := f x
+
+open Lean in
+example (n : Ident) : Term := n
+```
+
+In the case of {name}`th`, using {keywordOf Lean.Parser.Command.print}`#print` demonstrates that evaluation of the function application is delayed until the thunk's value is requested:
+```lean (name := thunkEval)
 #print th
-/-- info: instCoeTOfCoeHTCT -/
-#guard_msgs in
-#synth CoeT Lean.Name `ident Lean.SyntaxNodeKinds
 ```
+```leanOutput thunkEval
+def th : (Int → String) → Nat → Thunk String :=
+fun f x => { fn := fun x_1 => f ↑x }
+```
+:::
 
 
 ```lean (show := false)
@@ -234,6 +239,46 @@ instance : OfNat Bin n where
 ```
 ::::
 
+Most new coercions can be defined by declaring an instance of the {name}`Coe` {tech}[type class] and applying the {attr}`coe` attribute to the function that performs the coercion.
+To enable more control over coercions or to enable them in more contexts, Lean provides further classes that can be implemented, described in the rest of this chapter.
+
+:::example "Defining Coercions: Decimal Numbers"
+Decimal numbers can be defined as arrays of digits.
+
+```lean
+structure Decimal where
+  digits : Array (Fin 10)
+```
+
+Adding a coercion allows them to be used in contexts that expect {lean}`Nat`, but also contexts that expect any type that {lean}`Nat` can be coerced to.
+
+```lean
+@[coe]
+def Decimal.toNat (d : Decimal) : Nat :=
+  d.digits.foldl (init := 0) fun n d => n * 10 + d.val
+
+instance : Coe Decimal Nat where
+  coe := Decimal.toNat
+```
+
+This can be demonstrated by treating a {lean}`Decimal` as an {lean}`Int` as well as a {lean}`Nat`:
+```lean (name := digival)
+def twoHundredThirteen : Decimal where
+  digits := #[2, 1, 3]
+
+def one : Decimal where
+  digits := #[1]
+
+#eval (one : Int) - (twoHundredThirteen : Nat)
+```
+```leanOutput digival
+-212
+```
+
+:::
+
+{docstring Coe}
+
 
 
 # Coercion Insertion
@@ -245,11 +290,11 @@ tag := "coercion-insertion"
 The process of searching for a coercion from one type to another is called {deftech}_coercion insertion_.
 Coercion insertion is attempted in the following situations where an error would otherwise occur:
 
- * When the expected type for a term is not equal to the type found for the term
+ * The expected type for a term is not equal to the type found for the term.
 
- * When a type or proposition is expected, but the term's type is not a {tech}[universe]
+ * A type or proposition is expected, but the term's type is not a {tech}[universe].
 
- * When a term is applied as though it were a function, but its type is not a function type
+ * A term is applied as though it were a function, but its type is not a function type.
 
 Coercions are also inserted when they are explicitly requested.
 Each situation in which coercions may be inserted has a corresponding prefix operator that triggers the appropriate insertion.
@@ -569,8 +614,6 @@ end
 
 {docstring CoeOut}
 
-{docstring Coe}
-
 {docstring CoeTail}
 
 Instances of {name}`CoeT` can be synthesized when an appropriate chain of instances exists, or when there is a single applicable {name}`CoeDep` instance.