From 3443cfc33e203111234644580a95cdf8c6156c95 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 7 Feb 2025 07:31:22 +0100 Subject: [PATCH] better example flow --- CONTRIBUTING.md | 33 ++++++++++++++++++- Manual/Coercions.lean | 77 +++++++++++++++++++++++++++++++++---------- 2 files changed, 92 insertions(+), 18 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 503b559..44dfeb2 100644 --- a/CONTRIBUTING.md +++ b/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. diff --git a/Manual/Coercions.lean b/Manual/Coercions.lean index cd072a1..a1dfe8e 100644 --- a/Manual/Coercions.lean +++ b/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.