diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 71fca6dd..9902e269 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -95,6 +95,23 @@ jobs: echo "-----------" cat words.txt + - name: Preprocess HTML for prose linter + run: | + # First the HTML needs preprocessing to work well with Vale + pushd _out + python3 -m venv venv + . venv/bin/activate + pip install beautifulsoup4 + python ../.vale/scripts/rewrite_html.py html-multi html-vale + popd + + - name: Prose linter + uses: errata-ai/vale-action@v2.1.1 + with: + files: _out/html-vale/ + fail_on_error: true + filter_mode: nofilter + - name: Save word count run: | echo "# Word Counts" >> $GITHUB_STEP_SUMMARY diff --git a/.gitignore b/.gitignore index ac3770a8..a5d9f7c6 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,4 @@ figures/*.aux /figures/*.pdf /figures/*.svg /figures/auto/ +venv diff --git a/.vale.ini b/.vale.ini new file mode 100644 index 00000000..bea3ec73 --- /dev/null +++ b/.vale.ini @@ -0,0 +1,24 @@ +StylesPath = ".vale/styles" + +MinAlertLevel = suggestion + +Vocab = Lean + +# Inline-level tags to ignore +IgnoredScopes = code, tt + +# Block-level tags to ignore +SkippedScopes = script, style, pre, div + +# For now, ignore style warnings on included docstrings. It seems +# that vale is also not ignoring an entire tree, but only text +# immediately under the element with the tag, so we need some extra +# things here (e.g. a span under a code is not being ignored) +IgnoredClasses = namedocs, hl, token, goal-name, citation, TODO + + +[*] +BasedOnStyles = Vale, Lean + +# Lean has its own of these +Vale.Spelling = NO diff --git a/.vale/scripts/rewrite_html.py b/.vale/scripts/rewrite_html.py new file mode 100644 index 00000000..ed98ed53 --- /dev/null +++ b/.vale/scripts/rewrite_html.py @@ -0,0 +1,75 @@ +import os +import sys +import re +from bs4 import BeautifulSoup + +section_number_pattern = re.compile(r"^\s*(\d+\.)+\s*") + +def process_html_file(filepath, output_filepath): + """Reads an HTML file, removes 'QA' from headers, and writes the result to the output path.""" + with open(filepath, 'r', encoding='utf-8') as file: + soup = BeautifulSoup(file, 'html.parser') + + # Simplify all header tags + for header_tag in soup.find_all(['h1', 'h2', 'h3', 'h4', 'h5', 'h6']): + if header_tag.contents: + start = header_tag.contents[0] + if start.string: + no_num = section_number_pattern.sub("", start.string) + header_tag.contents[0].replace_with(no_num) + for other in header_tag.find_all(['span'], class_="permalink-widget"): + other.decompose() + header_tag.replace_with(header_tag.get_text()) + + # Simplify ordinal idiom + for code_tag in soup.find_all('code'): + # Check if the tag is followed directly by 'th' + if code_tag.next_sibling and code_tag.next_sibling.string and code_tag.next_sibling.string.startswith('th'): + # Replace XYZth with '5th' + code_tag.replace_with("5") + + # Delete docstring content (for now) + for element in soup.find_all(class_="namedocs"): + element.decompose() + + # Replace citations with their text + for element in soup.find_all(class_="citation"): + for inner in element.contents: + inner.replace_with(inner.get_text()) + + # Ensure the output directory exists + os.makedirs(os.path.dirname(output_filepath), exist_ok=True) + + # Write the modified HTML to the new output location + with open(output_filepath, 'w', encoding='utf-8') as file: + file.write(str(soup)) + +def traverse_directory(source_directory, output_directory): + """Recursively traverses source directory, processes HTML files, and writes them to output directory.""" + for root, _, files in os.walk(source_directory): + for filename in files: + if filename.endswith('.html') or filename.endswith('.htm'): + filepath = os.path.join(root, filename) + # Create the equivalent path in the output directory + relative_path = os.path.relpath(filepath, source_directory) + output_filepath = os.path.join(output_directory, relative_path) + + print(f"Processing {filepath} -> {output_filepath}") + process_html_file(filepath, output_filepath) + +if __name__ == "__main__": + # Check for command-line arguments + if len(sys.argv) != 3: + print("Usage: python script.py ") + sys.exit(1) + + # Get source and output directories from command-line arguments + source_directory = sys.argv[1] + output_directory = sys.argv[2] + + if not os.path.isdir(source_directory): + print("The provided source path is not a directory or does not exist.") + sys.exit(1) + + traverse_directory(source_directory, output_directory) + print("Processing complete.") diff --git a/.vale/styles/Lean/Capitalization.yml b/.vale/styles/Lean/Capitalization.yml new file mode 100644 index 00000000..87ea485f --- /dev/null +++ b/.vale/styles/Lean/Capitalization.yml @@ -0,0 +1,7 @@ +extends: substitution +message: Use '%s' instead of '%s' +level: error +ignorecase: false +swap: + 'unicode': 'Unicode' + 'javascript': 'JavaScript' diff --git a/.vale/styles/Lean/Latin.yml b/.vale/styles/Lean/Latin.yml new file mode 100644 index 00000000..f42b06bc --- /dev/null +++ b/.vale/styles/Lean/Latin.yml @@ -0,0 +1,6 @@ +extends: substitution +message: The word 'se' should occur as part of 'per se'. Use '%s' instead of '%s'. +level: error +ignorecase: true +swap: + - '(?:[^\s]*) se\b': 'per se' diff --git a/.vale/styles/Lean/Names.yml b/.vale/styles/Lean/Names.yml new file mode 100644 index 00000000..802d5c28 --- /dev/null +++ b/.vale/styles/Lean/Names.yml @@ -0,0 +1,18 @@ +extends: substitution +message: Use '%s' instead of '%s'. +level: error +ignorecase: true +swap: + - 'de moura': 'de Moura' + - 'blott': 'Blott' + - 'carneiro': 'Carneiro' + - 'lua': 'Lua' + - 'Madelaine': 'Madelaine' + - 'mathlib': 'Mathlib' + - 'merkin': 'Merkin' + - 'peano': 'Peano' + - 'selsam': 'Selsam' + - 'simons': 'Simons' + - 'ullrich': 'Ullrich' + - 'wadler': 'Wadler' + diff --git a/.vale/styles/Lean/Spelling.yml b/.vale/styles/Lean/Spelling.yml new file mode 100644 index 00000000..fb06d2dd --- /dev/null +++ b/.vale/styles/Lean/Spelling.yml @@ -0,0 +1,9 @@ +extends: spelling +message: "Did you really mean '%s'?" +level: error +ignore: + - names.txt + - terms.txt + + + diff --git a/.vale/styles/Lean/TechnicalTerms.yml b/.vale/styles/Lean/TechnicalTerms.yml new file mode 100644 index 00000000..b670fd24 --- /dev/null +++ b/.vale/styles/Lean/TechnicalTerms.yml @@ -0,0 +1,21 @@ +extends: substitution +message: Use '%s' instead of '%s' +level: error +ignorecase: true +swap: + 'typeclass': 'type class' + 'typeclasses': 'type classes' + 'codepoint': 'code point' + 'multibyte': 'multi-byte' + 'iff': 'if and only if' + 'nonoverlapping': 'non-overlapping' + 'datatypes': 'types' + "datatype's": "type's" + 'precompiling': 'pre-compiling' + 'nonterminating': 'non-terminating' + 'nontermination': 'non-termination' + 'enum \b.+\b': 'enum inductive' + 'letterlike': 'letter-like' + 'semireducible': 'semi-reducible' + '\b(.+)\b simps': 'non-terminal simps' + '\babelian\b': 'Abelian' diff --git a/.vale/styles/Lean/Titles.yml b/.vale/styles/Lean/Titles.yml new file mode 100644 index 00000000..7d78543f --- /dev/null +++ b/.vale/styles/Lean/Titles.yml @@ -0,0 +1,8 @@ +extends: capitalization +message: "'%s' should be in title case: '%s'" +level: warning +scope: heading +match: $title +style: Chicago + + diff --git a/.vale/styles/config/ignore/names.txt b/.vale/styles/config/ignore/names.txt new file mode 100644 index 00000000..e0a56fef --- /dev/null +++ b/.vale/styles/config/ignore/names.txt @@ -0,0 +1,12 @@ +Blott +Carneiro +Lua +Madelaine +Mathlib +Merkin +Moura +Peano +Selsam +Simons +Ullrich +Wadler diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt new file mode 100644 index 00000000..10bf85f2 --- /dev/null +++ b/.vale/styles/config/ignore/terms.txt @@ -0,0 +1,101 @@ +Abelian +Packrat +accessor +accessors +bitvector +bitvectors +bitwise +callout +checkpointing +combinator +combinators +constructorless +conv +cumulative +cumulativity +definitionally +desugar +desugared +desugaring +disjointness +disjunct +disjuncts +elaborator +elaborator's +elaborators +enum +equational +extensional +extensionality +guillemet +guillemets +hoc +impredicative +impredicativity +initializer +initializers +injectivity +interoperate +interoperates +iterator +iterator's +iterators +letterlike +lookup +lookups +memoization +metaprogram +metaprogramming +metaprograms +metatheoretic +metavariable +metavariable's +metavariables +monoid +monomorphic +monomorphism +multiset +multisets +namespace +namespaces +nullary +parameters' +polymorphic +polymorphically +predicative +predicativity +prepending +propositionally +recursor +recursor's +recursors +scrutinee +scrutinees +se +semigroup +semireducible +simp +simps +simproc +simprocs +subgoal +subgoals +subproblem +subproblems +subsingleton +subsingletons +substring +substrings +subterm +subterms +subtree +subtrees +subtype +subtyping +syntaxes +toolchain +toolchain's +toolchains +unary +unescaped +uninstantiated diff --git a/.vale/styles/config/vocabularies/Lean/accept.txt b/.vale/styles/config/vocabularies/Lean/accept.txt new file mode 100644 index 00000000..e69de29b diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2f224cf4..900a5338 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -20,3 +20,36 @@ Please remember to get in touch ahead of time to plan a contribution. In general * 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. * One sentence per line, to make diffs easier to follow. + +## CI + +The CI requires that various checks are passed. + +One of them is that the text must live up to a number of rules written with Vale. The style implementation is still quite incomplete; just because your prose passes the linter doesn't mean it will necessarily be accepted! + +To run the check, first install Vale. The next step is to preprocess the generated HTML to remove features that Vale can't cope with. Finally, Vale itself can be run. + +To preprocess the HTML, use the script `.vale/scripts/rewrite_html.py`. It requires BeautifulSoup, so here's the overall steps to get it working the first time: + +``` +$ cd .vale/scripts +$ python3 -m venv venv +$ . ./venv/bin/activate # or the appropriate script for your shell, e.g. activate.fish +$ pip install beautifulsoup4 +``` +After that, just run +``` +$ . .vale/scripts/venv/bin/activate +``` +to set up the Python environment. + +The next step is to run this on Verso's output. If it's in `_out/html-multi`, do this via: +``` +$ cd _out +$ python ../.vale/scripts/rewrite_html.py html-multi html-vale +``` + +Now, run `vale`: +``` +$ vale html-vale +``` diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean index b1d424c2..94f618bc 100644 --- a/Manual/BasicTypes.lean +++ b/Manual/BasicTypes.lean @@ -23,7 +23,7 @@ tag := "basic-types" %%% -Lean includes a number of built-in datatypes that are specially supported by the compiler. +Lean includes a number of built-in types that are specially supported by the compiler. Some, such as {lean}`Nat`, additionally have special support in the kernel. Other types don't have special compiler support _per se_, but rely in important ways on the internal representation of types for performance reasons. @@ -99,7 +99,7 @@ tag := "char-runtime" %%% -In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a datatype or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed. +In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a constructor or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed. ## API Reference diff --git a/Manual/BasicTypes/Nat.lean b/Manual/BasicTypes/Nat.lean index cbf18224..bdc28964 100644 --- a/Manual/BasicTypes/Nat.lean +++ b/Manual/BasicTypes/Nat.lean @@ -21,7 +21,7 @@ The natural numbers are nonnegative integers. Logically, they are the numbers 0, 1, 2, 3, …, generated from the constructors {lean}`Nat.zero` and {lean}`Nat.succ`. Lean imposes no upper bound on the representation of natural numbers other than physical constraints imposed by the available memory of the computer. -Because the natural numbers are fundamental to both mathematical reasoning and programming, they are specially supported by Lean's implementation. The logical model of the natural numbers is as an inductive datatype, and arithmetic operations are specified using this model. In Lean's kernel, the interpreter, and compiled code, closed natural numbers are represented as efficient arbitrary-precision integers. Sufficiently small numbers are immediate values that don't require indirection through a pointer. Arithmetic operations are implemented by primitives that take advantage of the efficient representations. +Because the natural numbers are fundamental to both mathematical reasoning and programming, they are specially supported by Lean's implementation. The logical model of the natural numbers is as an {tech}[inductive type], and arithmetic operations are specified using this model. In Lean's kernel, the interpreter, and compiled code, closed natural numbers are represented as efficient arbitrary-precision integers. Sufficiently small numbers are immediate values that don't require indirection through a pointer. Arithmetic operations are implemented by primitives that take advantage of the efficient representations. # Logical Model %%% @@ -79,7 +79,7 @@ tag := "nat-performance" Using Lean's built-in arithmetic operators, rather than redefining them, is essential. The logical model of {lean}`Nat` is essentially a linked list, so addition would take time linear in the size of one argument. -Still worse, multiplication takes quadradic time in this model. +Still worse, multiplication takes quadratic time in this model. While defining arithmetic from scratch can be a useful learning exercise, these redefined operations will not be nearly as fast. # Syntax diff --git a/Manual/BasicTypes/String.lean b/Manual/BasicTypes/String.lean index b1b8d31d..40643f36 100644 --- a/Manual/BasicTypes/String.lean +++ b/Manual/BasicTypes/String.lean @@ -60,7 +60,7 @@ After the object header, a string contains: : length - The length of the encoded string, which may be shorter than the byte count due to UTF-8 multibyte characters + The length of the encoded string, which may be shorter than the byte count due to UTF-8 multi-byte characters : data diff --git a/Manual/BasicTypes/String/Literals.lean b/Manual/BasicTypes/String/Literals.lean index f55671a8..7269359d 100644 --- a/Manual/BasicTypes/String/Literals.lean +++ b/Manual/BasicTypes/String/Literals.lean @@ -37,11 +37,11 @@ The following forms of escape sequences are accepted: : `\xNN` - When `NN` is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode codepoint is indicated by the two-digit hexadecimal code. + When `NN` is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode code point is indicated by the two-digit hexadecimal code. : `\uNNNN` - When `NN` is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode codepoint is indicated by the four-digit hexadecimal code. + When `NN` is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode code point is indicated by the four-digit hexadecimal code. String literals may contain {deftech}[_gaps_]. diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index 2b4c494f..602b8977 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -46,7 +46,7 @@ Roughly speaking, Lean's processing of a source file can be divided into the fol : Parsing The parser transforms sequences of characters into syntax trees of type {lean}`Syntax`. - Lean's parser is extensible, so the {lean}`Syntax` datatype is very general. + Lean's parser is extensible, so the {lean}`Syntax` type is very general. : Macro Expansion @@ -77,7 +77,7 @@ In reality, the stages described above do not strictly occur one after the other Lean parses a single {tech}[command] (top-level declaration), elaborates it, and performs any necessary kernel checks. Macro expansion is part of elaboration; before translating a piece of syntax, the elaborator first expands any macros present at the outermost layer. Macro syntax may remain at deeper layers, but it will be expanded when the elaborator reaches those layers. -There are multiple kinds of elaboration: command elaboration implements the effects of each top-level command (e.g. declaring datatypes, saving definitions, evaluating expressions), while term elaboration is responsible for constructing the terms that occur in many commands (e.g. types in signatures, the right-hand sides of definitions, or expressions to be evaluated). +There are multiple kinds of elaboration: command elaboration implements the effects of each top-level command (e.g. declaring {tech}[inductive types], saving definitions, evaluating expressions), while term elaboration is responsible for constructing the terms that occur in many commands (e.g. types in signatures, the right-hand sides of definitions, or expressions to be evaluated). Tactic execution is a specialization of term elaboration. When a command is elaborated, the state of Lean changes. @@ -135,7 +135,7 @@ New macros may be added to the macro table. Defining new macros is described in detail in {ref "macros"}[the section on macros]. After macro expansion, both the term and command elaborators consult tables that map syntax kinds to elaboration procedures. -Term elaborators map syntax and an optional expected type to a core language expression using the very featureful monad mentioned above. +Term elaborators map syntax and an optional expected type to a core language expression using the very powerful monad mentioned above. Command elaborators accept syntax and return no value, but may have monadic side effects on the global command state. While both term and command elaborators have access to {lean}`IO`, it's unusual that they perform side effects; exceptions include interactions with external tools or solvers. @@ -174,7 +174,7 @@ There are independent re-implementations in [Rust](https://github.com/ammkrn/nan The language implemented by the kernel is a version of the Calculus of Constructions, a dependent type theory with the following features: * Full dependent types - * Inductively-defined datatypes that may be mutually inductive or include recursion nested under other inductive types + * Inductively-defined types that may be mutually inductive or include recursion nested under other inductive types * An {tech}[impredicative], definitionally proof-irrelevant, extensional {tech}[universe] of {tech}[propositions] * A {tech}[predicative], non-cumulative hierarchy of universes of data * {ref "quotients"}[Quotient types] with a definitional computation rule @@ -209,9 +209,9 @@ The presence of explicit proof terms makes it feasible to implement independent It is described in detail by {citet carneiro19}[] and {citet ullrich23}[]. Lean's type theory does not feature subject reduction, the definitional equality is not necessarily transitive, and it is possible to make the type checker fail to terminate. -None of these metatheoretic properties cause problems in practice—failures of transitivity are exceedingly rare, and as far as we know, nontermination has not occurred except when crafting code specifically to exercise it. +None of these metatheoretic properties cause problems in practice—failures of transitivity are exceedingly rare, and as far as we know, non-termination has not occurred except when crafting code specifically to exercise it. Most importantly, logical soundness is not affected. -In practice, apparent nontermination is indistinguishable from sufficiently slow programs; the latter are the causes observed in the wild. +In practice, apparent non-ermination is indistinguishable from sufficiently slow programs; the latter are the causes observed in the wild. These metatheoretic properties are a result of having impredicativity, quotient types that compute, definitional proof irrelevance, and propositional extensionality; these features are immensely valuable both to support ordinary mathematical practice and to enable automation. # Elaboration Results @@ -267,9 +267,9 @@ This split is for three reasons: * Translation to recursors does not necessarily preserve the cost model expected by programmers, in particular laziness vs strictness, but compiled code must have predictable performance. The compiler stores an intermediate representation in an environment extension. -For straightforwardly structurally recursive functions, the translation will use the datatype's recursor. +For straightforwardly structurally recursive functions, the translation will use the type's recursor. These functions tend to be relatively efficient when run in the kernel, their defining equations hold definitionally, and they are easy to understand. -Functions that use other patterns of recursion that cannot be captured by the datatype's recursor are translated using {deftech}[well-founded recursion], which is structural recursion on a proof that some measure decreases at each recursive call. +Functions that use other patterns of recursion that cannot be captured by the type's recursor are translated using {deftech}[well-founded recursion], which is structural recursion on a proof that some measure decreases at each recursive call. Lean can automatically derive many of these cases, but some require manual proofs. Well-founded recursion is more flexible, but the resulting functions are often slower to execute in the kernel due to the proof terms that show that a measure decreases, and their defining equations may hold only propositionally. To provide a uniform interface to functions defined via structural and well-founded recursion and to check its own correctness, the elaborator proves equational lemmas that relate the function to its original definition. @@ -335,7 +335,7 @@ def everyOther : List α → List α equational lemmas are generated that relate {lean}`everyOther`'s recursor-based implementation to its original recursive definition. -{lean}`everyOther.eq_unfold` states that a fully unapplied `everyOther` is equal to its unfolding: +{lean}`everyOther.eq_unfold` states that `everyOther` with no arguments is equal to its unfolding: ```signature everyOther.eq_unfold.{u} : @everyOther.{u} = fun {α} x => @@ -389,7 +389,7 @@ The contents of `.ilean` files are an implementation detail and may change at an Finally, the compiler is invoked to translate the intermediate representation of functions stored in its environment extension into C code. A C file is produced for each Lean module; these are then compiled to native code using a bundled C compiler. If the `precompileModules` option is set in the build configuration, then this native code can be dynamically loaded and invoked by Lean; otherwise, an interpreter is used. -For most workloads, the overhead of compilation is larger than the time saved by avoiding the interpreter, but some workloads can be sped up dramatically by precompiling tactics, language extensions, or other extensions to Lean. +For most workloads, the overhead of compilation is larger than the time saved by avoiding the interpreter, but some workloads can be sped up dramatically by pre-compiling tactics, language extensions, or other extensions to Lean. # Initialization diff --git a/Manual/Language.lean b/Manual/Language.lean index c04148bb..3bc34b1e 100644 --- a/Manual/Language.lean +++ b/Manual/Language.lean @@ -334,7 +334,7 @@ def Codec.char : Codec where Universe-polymorphic definitions in fact create a _schematic definition_ that can be instantiated at a variety of levels, and different instantiations of universes create incompatible values. -:::Manual.example "Universe polymorhism is not first-class" +:::Manual.example "Universe polymorphism is not first-class" This can be seen in the following example, in which `T` is a gratuitously-universe-polymorphic definition that always returns the constructor of the unit type. Both instantiations of `T` have the same value, and both have the same type, but their differing universe instantiations make them incompatible: @@ -488,7 +488,7 @@ def id₃ (α : Type u) (a : α) := a ``` ::: -Because automatic implicit arguments only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declared with `universe` even when `autoImplicit` is `true`. +Because the automatic implicit parameter feature only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declared with `universe` even when `autoImplicit` is `true`. :::Manual.example "Automatic universe parameters and the `universe` command" @@ -496,7 +496,7 @@ This definition with an explicit universe parameter is accepted: ```lean (keep := false) def L.{u} := List (Type u) ``` -Even with automatic implicits, this definition is rejected, because `u` is not mentioned in the header, which precedes the `:=`: +Even with automatic implicit parameters, this definition is rejected, because `u` is not mentioned in the header, which precedes the `:=`: ```lean (error := true) (name := unknownUni) (keep := false) set_option autoImplicit true def L := List (Type u) @@ -690,7 +690,7 @@ $_ Describe signatures, including the following topics: * Explicit, implicit, instance-implicit, and strict implicit parameter binders - * {deftech}_Automatic implicits_ + * {deftech}_Automatic implicit_ parameters * Argument names and by-name syntax * Which parts can be omitted where? Why? @@ -756,7 +756,7 @@ This section will describe the translation of {deftech}[well-founded recursion]. ## Controlling Reduction :::planned 58 -This section will describe {deftech}_reducibility_: {deftech}[reducible], {deftech}[semireducible], and {deftech}[irreducible] definitions. +This section will describe {deftech}_reducibility_: {deftech}[reducible], {deftech}[semi-reducible], and {deftech}[irreducible] definitions. ::: ## Partial and Unsafe Recursive Definitions diff --git a/Manual/Language/Classes.lean b/Manual/Language/Classes.lean index 8a2eee97..32c8f37e 100644 --- a/Manual/Language/Classes.lean +++ b/Manual/Language/Classes.lean @@ -62,7 +62,7 @@ All of these possibilities are used in practice: : Computational effects - Type classes such as {name}`Monad`, whose parameter is a function from one type to another, are used to provide {ref "monads-and-do"}[special syntax for effectful operations.] + Type classes such as {name}`Monad`, whose parameter is a function from one type to another, are used to provide {ref "monads-and-do"}[special syntax for programs with side effects.] The “type” for which operations are overloaded is actually a type-level function, such as {name}`Option`, {name}`IO`, or {name}`Except`. : Predicates and propositions @@ -82,7 +82,7 @@ Here are some typical use cases for type classes: * A type class can represent a relation between two types that allows them to be used together in some novel way by a library. The {lean}`Coe` class represents automatically-inserted coercions from one type to another, and {lean}`MonadLift` represents a way to run operations with one kind of effect in a context that expects another kind. * Type classes can represent a framework of type-driven code generation, where instances for polymorphic types each contribute some portion of a final program. - The {name}`Repr` class defines a canonical pretty-printer for a datatype, and polymorphic types end up with polymorphic {name}`Repr` instances. + The {name}`Repr` class defines a canonical pretty-printer for a type, and polymorphic types end up with polymorphic {name}`Repr` instances. When pretty printing is finally invoked on an expression with a known concrete type, such as {lean}`List (Nat × (String ⊕ Int))`, the resulting pretty printer contains code assembled from the {name}`Repr` instances for {name}`List`, {name}`Prod`, {name}`Nat`, {name}`Sum`, {name}`String`, and {name}`Int`. # Class Declarations @@ -138,7 +138,7 @@ The differences between structure and class declarations are: : Registered as class - The resulting datatype is registered as a type class, for which instances may be defined and that may be used as the type of instance-implicit arguments. + The resulting inductive type is registered as a type class, for which instances may be defined and that may be used as the type of instance-implicit arguments. : Out and semi-out parameters are considered @@ -283,7 +283,7 @@ def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α := The problem is that a heap constructed with one {name}`Ord` instance may later be used with another, leading to the breaking of the heap invariant. -One way to correct this is to making the heap datatype depend on the selected `Ord` instance: +One way to correct this is to making the heap type depend on the selected `Ord` instance: ```lean structure Heap' (α : Type u) [Ord α] where contents : Array α diff --git a/Manual/Language/Classes/DerivingHandlers.lean b/Manual/Language/Classes/DerivingHandlers.lean index 06953d17..8d10d000 100644 --- a/Manual/Language/Classes/DerivingHandlers.lean +++ b/Manual/Language/Classes/DerivingHandlers.lean @@ -71,7 +71,7 @@ class IsEnum (α : Type) where from_to_id : ∀ (x : α), fromIdx (toIdx x) = x ``` -For datatypes that are trivial enumerations, where no constructor expects any parameters, instances of this class are quite repetitive. +For inductive types that are trivial enumerations, where no constructor expects any parameters, instances of this class are quite repetitive. The instance for `Bool` is typical: ```lean instance : IsEnum Bool where diff --git a/Manual/Language/Classes/InstanceDecls.lean b/Manual/Language/Classes/InstanceDecls.lean index b6cfba6b..13d1d77e 100644 --- a/Manual/Language/Classes/InstanceDecls.lean +++ b/Manual/Language/Classes/InstanceDecls.lean @@ -119,7 +119,7 @@ Functions defined in {keywordOf Lean.Parser.Command.declaration}`where` structur Because instance declaration is a version of structure definition, type class methods are also not recursive by default. Instances for recursive inductive types are common, however. There is a standard idiom to work around this limitation: define a recursive function independently of the instance, and then refer to it in the instance definition. -By convention, these recursive functions have the name of the corresponding method, but are defined in the datatype's namespace. +By convention, these recursive functions have the name of the corresponding method, but are defined in the type's namespace. ::: example "Instances are not recursive" Given this definition of {lean}`NatTree`: @@ -173,7 +173,7 @@ inductive NatRoseTree where | node (val : Nat) (children : Array NatRoseTree) ``` -Checking the equality of rose trees requires checking equality of of arrays. +Checking the equality of rose trees requires checking equality of arrays. However, instances are not typically available for instance synthesis during their own definitions, so the following definition fails, even though {lean}`NatRoseTree.beq` is a recursive function and is in scope in its own definition. ```lean (error := true) (name := natRoseTreeBEqFail) (keep := false) def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool @@ -205,7 +205,7 @@ tag := "class-inductive-instances" %%% Many instances have function types: any instance that itself recursively invokes instance search is a function, as is any instance with implicit parameters. -While most instances only project method implementations from their own instance parameters, instances of class inductives typically pattern-match one or more of their arguments, allowing the instance to select the appropriate constructor. +While most instances only project method implementations from their own instance parameters, instances of class inductive types typically pattern-match one or more of their arguments, allowing the instance to select the appropriate constructor. This is done using ordinary Lean function syntax. Just as with other instances, the function in question is not available for instance synthesis in its own definition. ::::keepEnv diff --git a/Manual/Language/Classes/InstanceSynth.lean b/Manual/Language/Classes/InstanceSynth.lean index 686b7245..7894d070 100644 --- a/Manual/Language/Classes/InstanceSynth.lean +++ b/Manual/Language/Classes/InstanceSynth.lean @@ -27,7 +27,7 @@ tag := "instance-synth" Instance synthesis is a recursive search procedure that either finds an instance for a given type class or fails. In other words, given a type that is registered as a type class, instance synthesis attempts constructs a term with said type. -It respects {tech}[reducibility]: {tech}[semireducible] or {tech}[irreducible] definitions are not unfolded, so instances for a definition are not automatically treated as instances for its unfolding unless it is {tech}[reducible]. +It respects {tech}[reducibility]: {tech}[semi-reducible] or {tech}[irreducible] definitions are not unfolded, so instances for a definition are not automatically treated as instances for its unfolding unless it is {tech}[reducible]. There may be multiple possible instances for a given class; in this case, declared priorities and order of declaration are used as tiebreakers, in that order, with more recent instances taking precedence over earlier ones with the same priority. This search procedure is efficient in the presence of diamonds and does not loop indefinitely when there are cycles. diff --git a/Manual/Language/Files.lean b/Manual/Language/Files.lean index 3dd88527..054cd124 100644 --- a/Manual/Language/Files.lean +++ b/Manual/Language/Files.lean @@ -51,7 +51,7 @@ tag := "module-syntax" Lean's concrete syntax is extensible. -In a language like Lean, it's not possible to completely describe the syntax once and for all, because libraries may define syntax in addition to new constants or datatypes. +In a language like Lean, it's not possible to completely describe the syntax once and for all, because libraries may define syntax in addition to new constants or {tech}[inductive types]. Rather than completely describing the language here, the overall framework is described, while the syntax of each language construct is documented in the section to which it belongs. ### Whitespace @@ -89,9 +89,9 @@ tag := "keywords-and-identifiers" An {deftech}[identifier] consists of one or more identifier components, separated by `'.'`.{index}[identifier] -{deftech}[Identifier components] consist of a letter or letterlike character or an underscore (`'_'`), followed by zero or more identifier continuation characters. -Letters are English letters, upper- or lowercase, and the letterlike characters include a range of non-English alphabetic scripts, including the Greek script which is widely used in Lean, as well as the members of the Unicode letterlike symbol block, which contains a number of double-struck characters (including `ℕ` and `ℤ`) and abbreviations. -Identifier continuation characters consist of letters, letterlike characters, underscore (`'_'`), exclamation mark (`!`), question mark (`?`), subscripts, and single quotes (`'`). +{deftech}[Identifier components] consist of a letter or letter-like character or an underscore (`'_'`), followed by zero or more identifier continuation characters. +Letters are English letters, upper- or lowercase, and the letter-like characters include a range of non-English alphabetic scripts, including the Greek script which is widely used in Lean, as well as the members of the Unicode letter-like symbol block, which contains a number of double-struck characters (including `ℕ` and `ℤ`) and abbreviations. +Identifier continuation characters consist of letters, letter-like characters, underscore (`'_'`), exclamation mark (`!`), question mark (`?`), subscripts, and single quotes (`'`). As an exception, underscore alone is not a valid identifier. ````lean (show := false) @@ -163,7 +163,7 @@ Such identifier components may contain any character at all, aside from `'»'`, Some potential identifier components may be reserved keywords. The specific set of reserved keywords depends on the set of active syntax extensions, which may depend on the set of imported modules and the currently-opened {TODO}[xref/deftech for namespace] namespaces; it is impossible to enumerate for Lean as a whole. These keywords must also be quoted with guillemets to be used as identifier components in most syntactic contexts. -Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are {deftech}_raw identifier_ contexts.{index (subterm:="raw")}[identifier] +Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive types, are {deftech}_raw identifier_ contexts.{index (subterm:="raw")}[identifier] Identifiers that contain one or more `'.'` characters, and thus consist of more than one identifier component, are called {deftech}[hierarchical identifiers]. Hierarchical identifiers are used to represent both module names and names in a namespace. @@ -249,7 +249,7 @@ tag := "module-contents" %%% -A module includes an {TODO}[def and xref] environment, which includes both the datatype and constant definitions from an environment and any data stored in {TODO}[xref] its environment extensions. +A module includes an {TODO}[def and xref] environment, which includes both the inductive type and constant definitions from an environment and any data stored in {TODO}[xref] its environment extensions. As the module is processed by Lean, commands add content to the environment. A module's environment can be serialized to a {deftech (key:="olean")}[`.olean` file], which contains both the environment and a compacted heap region with the run-time objects needed by the environment. This means that an imported module can be loaded without re-executing all of its commands. diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean index dc0a3df6..1f3a3162 100644 --- a/Manual/Language/Functions.lean +++ b/Manual/Language/Functions.lean @@ -370,7 +370,7 @@ tag := "totality" Functions can be defined recursively using {keywordOf Lean.Parser.Command.declaration}`def`. -From the perspective of Lean's logic, all functions are {deftech}_total_, meaning that they map each element of the domain to an element of the range in finite time.{margin}[Some programming language communities use the term _total_ in a more restricted sense, where functions are considered total if they do not crash but nontermination is ignored.] +From the perspective of Lean's logic, all functions are {deftech}_total_, meaning that they map each element of the domain to an element of the range in finite time.{margin}[Some programming language communities use the term _total_ in a more restricted sense, where functions are considered total if they do not crash but non-termination is ignored.] The values of total functions are defined for all type-correct arguments, and they cannot fail to terminate or crash due to a missing case in a pattern match. While the logical model of Lean considers all functions to be total, Lean is also a practical programming language that provides certain "escape hatches". diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean index f8f1dc42..33f6faa6 100644 --- a/Manual/Language/InductiveTypes.lean +++ b/Manual/Language/InductiveTypes.lean @@ -31,7 +31,7 @@ Inductive types may have any number of constructors; these constructors introduc Based on the type constructor and the constructors for an inductive type, Lean derives a {deftech}_recursor_{index}[recursor]{see "recursor"}[eliminator]. Logically, recursors represent induction principles or elimination rules; computationally, they represent primitive recursive computations. The termination of recursive functions is justified by translating them into uses of the recursors, so Lean's kernel only needs to perform type checking of recursor applications, rather than including a separate termination analysis. -Lean additionally produces a number of helper constructions based on the recursor,{margin}[The term _recursor_ is always used, even for non-recursive datatypes.] which are used elsewhere in the system. +Lean additionally produces a number of helper constructions based on the recursor,{margin}[The term _recursor_ is always used, even for non-recursive types.] which are used elsewhere in the system. _Structures_ are a special case of inductive types that have exactly one constructor. @@ -66,7 +66,7 @@ If no signature is provided, then Lean will attempt to infer a universe that's j In some situations, this process may fail to find a minimal universe or fail to find one at all, necessitating an annotation. The constructor specifications follow {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where`. -Constructors are not mandatory, as constructorless datatypes such as {lean}`False` and {lean}`Empty` are perfectly sensible. +Constructors are not mandatory, as constructorless inductive types such as {lean}`False` and {lean}`Empty` are perfectly sensible. Each constructor specification begins with a vertical bar (`'|'`, Unicode `'VERTICAL BAR' (U+007c)`), declaration modifiers, and a name. The name is a {tech}[raw identifier]. A declaration signature follows the name. @@ -104,12 +104,12 @@ tag := "example-inductive-types" %%% :::example "A constructorless type" -{lean}`Vacant` is an empty datatype, equivalent to Lean's {lean}`Empty` type: +{lean}`Vacant` is an empty inductive type, equivalent to Lean's {lean}`Empty` type: ```lean inductive Vacant : Type where ``` -Empty datatypes are not useless; they can be used to indicate unreachable code. +Empty inductive types are not useless; they can be used to indicate unreachable code. ::: :::example "A constructorless proposition" @@ -365,7 +365,7 @@ axiom α : Prop * {lean}`Decidable α` is represented the same way as `Bool` {TODO}[Aren't Decidable and Bool just special cases of the rules for trivial constructors and irrelevance?] - * {lean}`Nat` is represented by `lean_object *`. Its run-time value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is `1` (checked by `lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`). {TODO}[Move these to FFI section or Nat chapter] + * {lean}`Nat` is represented by `lean_object *`. Its run-time value is either a pointer to an opaque arbitrary-precision integer object or, if the lowest bit of the “pointer” is `1` (checked by `lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`). {TODO}[Move these to FFI section or Nat chapter] ::: ## Relevance @@ -447,7 +447,7 @@ The memory order of the fields is derived from the types and order of the fields Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose. * To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field. -* To access {lean}`USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind. +* To access {lean}`USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th `USize` field and `n` is the total number of fields of the first kind. * To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds. ::::keepEnv @@ -503,7 +503,7 @@ Mutually recursive definitions of inductive types are specified by defining the :::example "Mutually Defined Inductive Types" The type {name}`EvenOddList` in a prior example used a Boolean index to select whether the list in question should have an even or odd number of elements. -This distinction can also be expressed by the choice of one of two mutually inductive datatypes {name}`EvenList` and {name}`OddList`: +This distinction can also be expressed by the choice of one of two mutually inductive types {name}`EvenList` and {name}`OddList`: ```lean mutual @@ -706,7 +706,7 @@ tag := "mutual-inductive-types-positivity" %%% Each inductive type that is defined in the `mutual` group may occur only strictly positively in the types of the parameters of the constructors of all the types in the group. -In other words, in the type of each parameter to each constructor in all the types of the group, none of the type constructors in the group occur to the left of any arrows, and none of them occur in argument positions unless they are an argument to an inductive datatype's type constructor. +In other words, in the type of each parameter to each constructor in all the types of the group, none of the type constructors in the group occur to the left of any arrows, and none of them occur in argument positions unless they are an argument to an inductive type's type constructor. ::: example "Mutual strict positivity" In the following mutual group, `Tm` occurs in a negative position in the argument to `Binding.scope`: diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean index cb498344..4892c8b0 100644 --- a/Manual/Language/InductiveTypes/LogicalModel.lean +++ b/Manual/Language/InductiveTypes/LogicalModel.lean @@ -56,7 +56,7 @@ The result type of the recursor is the motive applied to these indices and the t :::example "The recursor for {lean}`Bool`" {lean}`Bool`'s recursor {name}`Bool.rec` has the following parameters: - * The motive computes a type in any universe, given a Bool. + * The motive computes a type in any universe, given a {lean}`Bool`. * There are cases for both constructors, in which the motive is satisfied for both {lean}`false` and {lean}`true`. * The target is some {lean}`Bool`. @@ -168,7 +168,7 @@ This is because it is not mentioned in any further parameters' types, so it coul :::example "{name}`And` is a subsingleton" -{lean}`And` is a subsingleton because it has one constructor, and both of the constructor's parameters's types are propositions. +{lean}`And` is a subsingleton because it has one constructor, and both of the constructor's parameters' types are propositions. Its recursor has the following signature: ```signature And.rec.{u} {a b : Prop} {motive : a ∧ b → Sort u} @@ -213,7 +213,7 @@ tag := "iota-reduction" %%% -In addition to adding new constants to the logic, inductive datatype declarations also add new reduction rules. +In addition to adding new constants to the logic, inductive type declarations also add new reduction rules. These rules govern the interaction between recursors and constructors; specifically recursors that have constructors as their targets. This form of reduction is called {deftech}_ι-reduction_ (iota reduction){index}[ι-reduction]{index (subterm:="ι (iota)")}[reduction]. @@ -225,7 +225,7 @@ If there are recursive parameters, then these arguments to the case are found by tag := "well-formed-inductives" %%% -Inductive datatype declarations are subject to a number of well-formedness requirements. +Inductive type declarations are subject to a number of well-formedness requirements. These requirements ensure that Lean remains consistent as a logic when it is extended with the inductive type's new rules. They are conservative: there exist potential inductive types that do not undermine consistency, but that these requirements nonetheless reject. @@ -273,7 +273,7 @@ This restriction rules out unsound inductive type definitions, at the cost of al :::::example "Non-strictly-positive inductive types" ::::keepEnv -The datatype `Bad` would make Lean inconsistent if it were not rejected: +The type `Bad` would make Lean inconsistent if it were not rejected: ```lean (name := Bad) (error := true) inductive Bad where | bad : (Bad → Bad) → Bad @@ -321,7 +321,7 @@ Lean rejects universe-polymorphic types that could not, in practice, be used pol This could arise if certain instantiations of the universe parameters would cause the type itself to be a {lean}`Prop`. If this type is not a {tech}[subsingleton], then is recursor can only target propositions (that is, the {tech}[motive] must return a {lean}`Prop`). These types only really make sense as {lean}`Prop`s themselves, so the universe polymorphism is probably a mistake. -Because they are largely useless, Lean's datatype elaborator has not been designed to support these types. +Because they are largely useless, Lean's inductive type elaborator has not been designed to support these types. When such universe-polymorphic inductive types are indeed subsingletons, it can make sense to define them. Lean's standard library defines {name}`PUnit` and {name}`PEmpty`. diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean index 7dca1daa..ee892f1d 100644 --- a/Manual/Language/InductiveTypes/Structures.lean +++ b/Manual/Language/InductiveTypes/Structures.lean @@ -82,7 +82,7 @@ MyStructure.mk.{u, v} :::: -For each field, a {deftech}[projection function] is generated that extracts the field's value from the underlying datatype's constructor. +For each field, a {deftech}[projection function] is generated that extracts the field's value from the underlying type's constructor. This function is in the structure's name's namespace. Structure field projections are handled specially by the elaborator (as described in the {ref "structure-inheritance"}[section on structure inheritance]), which performs extra steps beyond looking up a namespace. When field types depend on prior fields, the types of the dependent projection functions are written in terms of earlier projections, rather than explicit pattern matching. @@ -156,7 +156,7 @@ Its constructor is named {name}`Palindrome.ofString`, rather than `Palindrome.mk ::: example "Modifiers on structure constructor" The structure {lean}`NatStringBimap` maintains a finite bijection between natural numbers and strings. It consists of a pair of maps, such that the keys each occur as values exactly once in the other map. -Because the constructor is private, code outside the defining module can't construct new instances and must use the provided API, which maintains the invariants of the datatype. +Because the constructor is private, code outside the defining module can't construct new instances and must use the provided API, which maintains the invariants of the type. Additionally, providing the default constructor name explicitly is an opportunity to attach a {tech}[documentation comment] to the constructor. ```lean diff --git a/Manual/Meta/Bibliography.lean b/Manual/Meta/Bibliography.lean index 675d5324..d2351509 100644 --- a/Manual/Meta/Bibliography.lean +++ b/Manual/Meta/Bibliography.lean @@ -141,7 +141,7 @@ where | other => #[other] -def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT ExtensionImpls IO) Html) (c : Citable) : HtmlT Manual (ReaderT ExtensionImpls IO) Html := open Html in do +def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT ExtensionImpls IO) Html) (c : Citable) : HtmlT Manual (ReaderT ExtensionImpls IO) Html := wrap <$> open Html in do match c with | .inProceedings p => let authors ← andList <$> p.authors.mapM go @@ -152,6 +152,7 @@ def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT Exte let authors ← andList <$> p.authors.mapM go return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". arXiv:" {{p.id}} }} where + wrap (content : Html) : Html := {{{{content}}}} link (title : Html) : Html := match c.url with | none => title diff --git a/Manual/Simp.lean b/Manual/Simp.lean index d0e33678..6b162bdb 100644 --- a/Manual/Simp.lean +++ b/Manual/Simp.lean @@ -202,7 +202,7 @@ The simplifier has three kinds of rewrite rules: : Declarations to unfold - The simplifier will only unfold {tech}[reducible] definitions by default. However, a rewrite rule can be added for any {tech}[semireducible] or {tech}[irreducible] definition that causes the simplifier to unfold it as well. When the simplifier is running in definitional mode ({tactic}`dsimp` and its variants), definition unfolding only replaces the defined name with its value; otherwise, it also uses the equational lemmas produced by the equation compiler. + The simplifier will only unfold {tech}[reducible] definitions by default. However, a rewrite rule can be added for any {tech}[semi-reducible] or {tech}[irreducible] definition that causes the simplifier to unfold it as well. When the simplifier is running in definitional mode ({tactic}`dsimp` and its variants), definition unfolding only replaces the defined name with its value; otherwise, it also uses the equational lemmas produced by the equation compiler. : Equational lemmas diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean index 128da10b..6e2f771e 100644 --- a/Manual/Tactics.lean +++ b/Manual/Tactics.lean @@ -112,7 +112,7 @@ intro n k :::: The {tactic}`case` and {tactic}`case'` tactics can be used to select a new main goal using the desired goal's name. -When names are assigned in the context of a goal which itself has a name, the new goals's names are appended to the main goal's name with a dot (`'.', Unicode FULL STOP (0x2e)`) between them. +When names are assigned in the context of a goal which itself has a name, the new goals' names are appended to the main goal's name with a dot (`'.', Unicode FULL STOP (0x2e)`) between them. ::::example "Hierarchical Goal Names" diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean index 4c6d93a5..50704ed6 100644 --- a/Manual/Tactics/Reference.lean +++ b/Manual/Tactics/Reference.lean @@ -18,6 +18,13 @@ set_option pp.rawOnError true set_option linter.unusedVariables false +def castPaper : ArXiv where + title := .concat (inlines!"Simplifying Casts and Coercions") + authors := #[.concat (inlines!"Robert Y. Lewis"), .concat (inlines!"Paul-Nicolas Madelaine")] + year := 2020 + id := "2001.10594" + + #doc (Manual) "Tactic Reference" => %%% tag := "tactic-ref" @@ -186,7 +193,7 @@ tag := "tactic-ref-casts" %%% The tactics in this section make it easier avoid getting stuck on {deftech}_casts_, which are functions that coerce data from one type to another, such as converting a natural number to the corresponding integer. -They are described in more detail in [_Simplifying Casts and Coercions_](https://arxiv.org/abs/2001.10594) by Robert Y. Lewis and Paul-Nicolas Madelaine. +They are described in more detail by {citet castPaper}[]. :::tactic Lean.Parser.Tactic.tacticNorm_cast_ :::