chore: add section introductions and planned content tags (#111)

Add links from unwritten sections to tracking issues where users can
give prioritization and content feedback.

Author: david-christiansen

Manual.lean

@@ -19,6 +19,9 @@ set_option pp.rawOnError true
 
 #doc (Manual) "The Lean Language Reference" =>
 
+This is the _Lean Language Reference_, an in-progress reference work on Lean.
+It is intended to be a comprehensive, precise description of Lean: a reference work in which Lean users can look up detailed information, rather than a tutorial for new users.
+For other documentation, please refer to the [Lean documentation site](https://lean-lang.org/documentation/).
 
 {include Manual.Intro}
 
@@ -30,7 +33,17 @@ set_option pp.rawOnError true
 
 # Monads and `do`-Notation
 
+:::planned 102
+This chapter will describe `do`-notation in Lean:
+ * Desugaring of `do` and its associated control structures
+ * Comprehensive description of the syntax of `do`-notation
+ * Definition of being in the "same `do`-block"
+:::
+
 # IO
+:::planned 102
+This chapter will describe features for writing programs that can have side effects on the real world.
+:::
 
 {include 0 Manual.Tactics}
 
@@ -40,7 +53,15 @@ set_option pp.rawOnError true
 
 # Standard Library
 
+:::planned 109
+Overview of the standard library, including types from the prelude and those that require imports.
+:::
+
 ## Optional Values
+:::planned 110
+Describe {name}`Option`, including the default coercions and its API.
+:::
+
 
 # Notations and Macros
 %%%

Manual/BasicTypes.lean

@@ -26,11 +26,34 @@ Other types don't have special compiler support _per se_, but rely in important
 {include 0 Manual.BasicTypes.Nat}
 
 # Integers
+::: planned 104
+ * Compile-time and run-time characteristics, and how they're inherited from {lean}`Nat`
+ * API reference
+:::
 
 # Fixed-Precision Integer Types
 
+::: planned 105
+ * Compile-time and run-time characteristics for {lean}`UInt8`, {lean}`UInt16`, {lean}`UInt32`, {lean}`UInt64`
+ * API reference
+:::
+
+# Bitvectors
+
+:::planned 106
+ * Run-time and kernel representations of {name}`BitVec`
+ * API reference
+ * Cross-reference to TBW chapter on `bv_decide`
+:::
+
 # Floating-Point Numbers
 
+:::planned 107
+ * Run-time and kernel representations
+ * Precision, and whether it's platform-dependent
+ * Relationship between IEEE floats and decidable equality
+:::
+
 # Characters
 
 {docstring Char}
@@ -67,6 +90,13 @@ In monomorphic contexts, characters are represented as 32-bit immediate values.
 
 # Linked Lists
 
+::: planned 108
+ * Representation at compile time and run time
+ * API reference
+ * Literal syntax
+ * Constructor/pattern syntax
+:::
+
 # Arrays
 
 ::: planned 91

Manual/Intro.lean

@@ -71,6 +71,8 @@ The FRO currently has more than ten employees working to support the growth and
 
 # Typographical Conventions
 
+This document makes use of a number of typographical and layout conventions to indicate various aspects of the information being presented.
+
 ## Lean Code
 
 This document contains many Lean code examples.

Manual/Language.lean

@@ -24,7 +24,7 @@ set_option linter.unusedVariables false
 
 {include Manual.Language.Files}
 
-# Types
+# The Type System
 
 {deftech}_Terms_, also known as {deftech}_expressions_, are the fundamental units of meaning in Lean's core language.
 They are produced from user-written syntax by the {tech}[elaborator].
@@ -518,9 +518,10 @@ def L := List (Type 0)
 
 #### Universe Unification
 
-:::TODO
+:::planned 00
  * Rules for unification, properties of algorithm
  * Lack of injectivity
+ * Universe inference for unannotated inductive types
 :::
 
 {include 2 Language.InductiveTypes}
@@ -536,13 +537,28 @@ tag := "quotients"
  * Show the computation rule
 :::
 
-# Module Structure
+# Module Contents
 
+As described {ref "module-structure"}[in the section on the syntax of files], a Lean module consists of a header followed by a sequence of commands.
 
 ## Commands and Declarations
 
+After the header, every top-level phrase of a Lean module is a command.
+Commands may add new types, define new constants, or query Lean for information.
+Commands may even {ref "language-extension"}[change the syntax used to parse subsequent commands].
+
+::: planned 100
+ * Describe the various families of available commands (definition-like, `#eval`-like, etc).
+ * Refer to specific chapters that describe major commands, such as `inductive`.
+:::
+
 ### Definition-Like Commands
 
+::: planned 101
+ * Precise descriptions of these commands and their syntax
+ * Comparison of each kind of definition-like command to the others
+:::
+
 The following commands in Lean are definition-like: {TODO}[Render commands as their name (a la tactic index)]
  * {syntaxKind}`def`
  * {syntaxKind}`abbrev`

Manual/Language/Files.lean

@@ -12,6 +12,10 @@ open Verso.Genre Manual
 
 #doc (Manual) "Files" =>
 
+The smallest unit of compilation in Lean is a single {deftech}[module].
+Modules correspond to source files, and are imported into other modules based on their filenames.
+In other words, the names and folder structures of files are significant in Lean code.
+
 # Modules
 
 Every Lean file defines a module.
@@ -140,7 +144,9 @@ Identifiers that contain one or more `'.'` characters, and thus consist of more
 Hierarchical identifiers are used to represent both module names and names in a namespace.
 
 ## Structure
-
+%%%
+tag := "module-structure"
+%%%
 
 
 :::syntax Lean.Parser.Module.module (open := false)

Manual/Tactics.lean

@@ -486,6 +486,11 @@ However, with a few exceptions, the majority of tactics can be identified by a l
 
 ## Control Structures
 
+Strictly speaking, there is no fundamental distinction between control structures and other tactics.
+Any tactic is free to take others as arguments and arrange for their execution in any context that it sees fit.
+Even if a distinction is arbitrary, however, it can still be useful.
+The tactics in this section are those that resemble traditional control structures from programming, or those that _only_ recombine other tactics rather than making progress themselves.
+
 ### Success and Failure
 
 When run in a proof state, every tactic either succeeds or fails.