leanprover · david-christiansen · Oct 20, 2025 · Oct 20, 2025
diff --git a/book/.verso/verso-xref-manifest.json b/book/.verso/verso-xref-manifest.json
@@ -1,8 +1,7 @@
 {"version": 0,
  "sources":
  {"manual":
-  {"updated": "2025-10-16:12:58:47.024355000",
-   "updateFrequency": "manual",
+  {"updateFrequency": "manual",
    "shortName": "ref",
    "root": "https://lean-lang.org/doc/reference/4.23.0/",
    "longName": "Lean Language Reference"}},

diff --git a/book/FPLean/DependentTypes/IndexedFamilies.lean b/book/FPLean/DependentTypes/IndexedFamilies.lean
@@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples"
 set_option verso.exampleModule "Examples.DependentTypes"
 
 #doc (Manual) "Indexed Families" =>
+%%%
+tag := "indexed-families"
+%%%
 
 Polymorphic inductive types take type arguments.
 For instance, {moduleName}`List` takes an argument that determines the type of the entries in the list, and {moduleName}`Except` takes arguments that determine the types of the exceptions or values.
@@ -291,6 +294,10 @@ def Vect.zip : (n : Nat) → Vect α n → Vect β n → Vect (α × β) n
 ```
 
 # Exercises
+%%%
+tag := "indexed-families-exercises"
+%%%
+
 
 Getting a feel for programming with dependent types requires experience, and the exercises in this section are very important.
 For each exercise, try to see which mistakes the type checker can catch, and which ones it can't, by experimenting with the code as you go.

diff --git a/book/FPLean/DependentTypes/IndicesParametersUniverses.lean b/book/FPLean/DependentTypes/IndicesParametersUniverses.lean
@@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples"
 set_option verso.exampleModule "Examples.DependentTypes.IndicesParameters"
 
 #doc (Manual) "Indices, Parameters, and Universe Levels" =>
+%%%
+tag := "indices-parameters-universe-levels"
+%%%
 
 The distinction between indices and parameters of an inductive type is more than just a way to describe arguments to the type that either vary or do not between the constructors.
 Whether an argument to an inductive type is a parameter or an index also matters when it comes time to determine the relationships between their universe levels.

diff --git a/book/FPLean/DependentTypes/Pitfalls.lean b/book/FPLean/DependentTypes/Pitfalls.lean
@@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples"
 set_option verso.exampleModule "Examples.DependentTypes.Pitfalls"
 
 #doc (Manual) "Pitfalls of Programming with Dependent Types" =>
+%%%
+tag := "dependent-type-pitfalls"
+%%%
 
 The flexibility of dependent types allows more useful programs to be accepted by a type checker, because the language of types is expressive enough to describe variations that less-expressive type systems cannot.
 At the same time, the ability of dependent types to express very fine-grained specifications allows more buggy programs to be rejected by a type checker.
@@ -72,6 +75,9 @@ Behind the scenes, pattern matching on the first {anchorName appendL1}`Vect` imp
 Here, {lit}`n✝` represents the {anchorName moreNames}`Nat` that is one less than the argument {anchorName appendL1}`n`.
 
 # Definitional Equality
+%%%
+tag := "definitional-equality"
+%%%
 
 In the definition of {anchorName appendL3}`plusL`, there is a pattern case {anchorTerm plusL}`0, k => k`.
 This applies in the length used in the first placeholder, so another way to write the underscore's type {anchorTerm moreNames}`Vect α (Nat.plusL 0 k)` is {anchorTerm moreNames}`Vect α k`.
@@ -230,6 +236,9 @@ Exposing the internals of a function in a type means that refactoring the expose
 In particular, the fact that {anchorName appendL}`plusL` is used in the type of {anchorName appendL}`appendL` means that the definition of {anchorName appendL}`plusL` cannot be replaced by the otherwise-equivalent {anchorName plusR}`plusR`.
 
 # Getting Stuck on Addition
+%%%
+tag := "stuck-addition"
+%%%
 
 What happens if append is defined with {anchorName appendR}`plusR` instead?
 Beginning in the same way, with explicit lengths and placeholder underscores in each case, reveals the following useful error messages:
@@ -301,6 +310,9 @@ Getting it unstuck requires {ref "equality-and-ordering"}[propositional equality
 :::
 
 # Propositional Equality
+%%%
+tag := "propositional-equality"
+%%%
 
 Propositional equality is the mathematical statement that two expressions are equal.
 While definitional equality is a kind of ambient fact that Lean automatically checks when required, statements of propositional equality require explicit proofs.
@@ -476,6 +488,9 @@ def appendR : Vect α n → Vect α k → Vect α (n.plusR k)
 ```
 
 # Pros and Cons
+%%%
+tag := "dependent-types-pros-and-cons"
+%%%
 
 Indexed families have an important property: pattern matching on them affects definitional equality.
 For example, in the {anchorName Vect}`nil` case in a {kw}`match` expression on a {anchorTerm Vect}`Vect`, the length simply _becomes_ {anchorTerm moreNames}`0`.
@@ -509,6 +524,9 @@ Fluency in their use is an important part of knowing when to use them.
 
 
 # Exercises
+%%%
+tag := "dependent-type-pitfalls-exercises"
+%%%
 
  * Using a recursive function in the style of {anchorName plusR_succ_left}`plusR_succ_left`, prove that for all {anchorName moreNames}`Nat`s {anchorName exercises}`n` and {anchorName exercises}`k`, {anchorTerm exercises}`n.plusR k = n + k`.
  * Write a function on {anchorName moreNames}`Vect` for which {anchorName plusR}`plusR` is more natural than {anchorName plusL}`plusL`, where {anchorName plusL}`plusL` would require proofs to be used in the definition.
diff --git a/book/FPLean/DependentTypes/Summary.lean b/book/FPLean/DependentTypes/Summary.lean
@@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples"
 set_option verso.exampleModule "Examples.DependentTypes"
 
 #doc (Manual) "Summary" =>
+%%%
+tag := "dependent-types-summary"
+%%%
 
 # Dependent Types
+%%%
+tag := none
+%%%
 
 Dependent types, where types contain non-type code such as function calls and ordinary data constructors, lead to a massive increase in the expressive power of a type system.
 The ability to _compute_ a type from the _value_ of an argument means that the return type of a function can vary based on which argument is provided.
@@ -28,6 +34,9 @@ In these cases, pattern-matching gets “stuck” and does not proceed until or
 Type-level computation can be seen as a kind of partial evaluation, where only the parts of the program that are sufficiently known need to be evaluated and other parts are left alone.
 
 # The Universe Pattern
+%%%
+tag := none
+%%%
 
 A common pattern when working with dependent types is to section off some subset of the type system.
 For example, a database query library might be able to return varying-length strings, fixed-length strings, or numbers in certain ranges, but it will never return a function, a user-defined datatype, or an {anchorName otherEx}`IO` action.
@@ -43,6 +52,9 @@ Defining a custom universe has a number of advantages over using the types direc
 
 
 # Indexed Families
+%%%
+tag := none
+%%%
 
 Datatypes can take two separate kinds of arguments: _parameters_ are identical in each constructor of the datatype, while _indices_ may vary between constructors.
 For a given choice of index, only some constructors of the datatype are available.
@@ -65,6 +77,9 @@ Thirdly, running complicated code on large values during type checking can lead
 Avoiding these slowdowns for complicated programs can require specialized techniques.
 
 # Definitional and Propositional Equality
+%%%
+tag := none
+%%%
 
 Lean's type checker must, from time to time, check whether two types should be considered interchangeable.
 Because types can contain arbitrary programs, it must therefore be able to check arbitrary programs for equality.

diff --git a/book/FPLean/DependentTypes/TypedQueries.lean b/book/FPLean/DependentTypes/TypedQueries.lean
@@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples"
 set_option verso.exampleModule "Examples.DependentTypes.DB"
 
 #doc (Manual) "Worked Example: Typed Queries" =>
+%%%
+tag := "typed-queries"
+%%%
 
 Indexed families are very useful when building an API that is supposed to resemble some other language.
 They can be used to write a library of HTML constructors that don't permit generating invalid HTML, to encode the specific rules of a configuration file format, or to model complicated business constraints.
@@ -20,6 +23,10 @@ It is not a realistic system, however—databases are represented as linked list
 However, it is large enough to demonstrate useful principles and techniques.
 
 # A Universe of Data
+%%%
+tag := "typed-query-data-universe"
+%%%
+
 In this relational algebra, the base data that can be held in columns can have types {anchorName DBType}`Int`, {anchorName DBType}`String`, and {anchorName DBType}`Bool` and are described by the universe {anchorName DBType}`DBType`:
 
 ```anchor DBType
@@ -97,6 +104,9 @@ instance {t : DBType} : Repr t.asType where
 ```
 
 # Schemas and Tables
+%%%
+tag := "schemas"
+%%%
 
 A schema describes the name and type of each column in a database:
 
@@ -163,6 +173,9 @@ def waterfallDiary : Table waterfall := [
 ```
 
 ## Recursion and Universes, Revisited
+%%%
+tag := "recursion-universes-revisited"
+%%%
 
 The convenient structuring of rows as tuples comes at a cost: the fact that {anchorName Row}`Row` treats its two base cases separately means that functions that use {anchorName Row}`Row` in their types and are defined recursively over the codes (that, is the schema) need to make the same distinctions.
 One example of a case where this matters is an equality check that uses recursion over the schema to define a function that checks rows for equality.
@@ -262,6 +275,9 @@ In the second role, the constructors are used like {anchorName Naturals}`Nat`s t
 Programming with indexed families often requires the ability to switch fluently between both perspectives.
 
 ## Subschemas
+%%%
+tag := "subschemas"
+%%%
 
 One important operation in relational algebra is to _project_ a table or row into a smaller schema.
 Every column not present in the smaller schema is forgotten.
@@ -416,6 +432,9 @@ def Subschema.reflexive : (s : Schema) → Subschema s s
 
 
 ## Projecting Rows
+%%%
+tag := "projecting-rows"
+%%%
 
 Given evidence that {anchorName RowProj}`s'` is a subschema of {anchorName RowProj}`s`, a row in {anchorName RowProj}`s` can be projected into a row in {anchorName RowProj}`s'`.
 This is done using the evidence that {anchorName RowProj}`s'` is a subschema of {anchorName RowProj}`s`, which explains where each column of {anchorName RowProj}`s'` is found in {anchorName RowProj}`s`.
@@ -433,6 +452,9 @@ def Row.project (row : Row s) : (s' : Schema) → Subschema s' s → Row s'
 
 
 # Conditions and Selection
+%%%
+tag := "conditions-and-selection"
+%%%
 
 Projection removes unwanted columns from a table, but queries must also be able to remove unwanted rows.
 This operation is called _selection_.
@@ -515,6 +537,9 @@ false
 ```
 
 # Queries
+%%%
+tag := "typed-query-language"
+%%%
 
 The query language is based on relational algebra.
 In addition to tables, it includes the following operators:
@@ -572,11 +597,17 @@ def Schema.renameColumn : (s : Schema) → HasCol s n t → String → Schema
 ```
 
 # Executing Queries
+%%%
+tag := "executing-queries"
+%%%
 
 Executing queries requires a number of helper functions.
 The result of a query is a table; this means that each operation in the query language requires a corresponding implementation that works with tables.
 
 ## Cartesian Product
+%%%
+tag := "executing-cartesian-product"
+%%%
 
 Taking the Cartesian product of two tables is done by appending each row from the first table to each row from the second.
 First off, due to the structure of {anchorName Row}`Row`, adding a single column to a row requires pattern matching on its schema in order to determine whether the result will be a bare value or a tuple.
@@ -635,6 +666,9 @@ def Table.cartesianProduct (table1 : Table s1) (table2 : Table s2) :
 
 
 ## Difference
+%%%
+tag := "executing-difference"
+%%%
 
 Removing undesired rows from a table can be done using {anchorName misc}`List.filter`, which takes a list and a function that returns a {anchorName misc}`Bool`.
 A new list is returned that contains only the entries for which the function returns {anchorName misc}`true`.
@@ -656,6 +690,9 @@ def List.without [BEq α] (source banned : List α) : List α :=
 This will be used with the {anchorName BEqDBType}`BEq` instance for {anchorName Row}`Row` when interpreting queries.
 
 ## Renaming Columns
+%%%
+tag := "executing-renaming-columns"
+%%%
 Renaming a column in a row is done with a recursive function that traverses the row until the column in question is found, at which point the column with the new name gets the same value as the column with the old name:
 
 ```anchor renameRow
@@ -672,6 +709,9 @@ One difficulty in programming with indexed families is that when performance mat
 It takes a very careful, often brittle, design to eliminate these kinds of “re-indexing” functions.
 
 ## Prefixing Column Names
+%%%
+tag := "executing-prefixing-column-names"
+%%%
 
 Adding a prefix to column names is very similar to renaming a column.
 Instead of proceeding to a desired column and then returning, {anchorName prefixRow}`prefixRow` must process all columns:
@@ -688,6 +728,9 @@ This can be used with {anchorName misc}`List.map` in order to add a prefix to al
 Once again, this function only exists to change the type of a value.
 
 ## Putting the Pieces Together
+%%%
+tag := "query-exec-runner"
+%%%
 
 With all of these helpers defined, executing a query requires only a short recursive function:
 
@@ -758,6 +801,10 @@ Because the example data includes only waterfalls in the USA, executing the quer
 ```
 
 ## Errors You May Meet
+%%%
+tag := "typed-queries-error-messages"
+%%%
+
 
 Many potential errors are ruled out by the definition of {anchorName Query}`Query`.
 For instance, forgetting the added qualifier in {anchorTerm Query2}`"mountain.location"` yields a compile-time error that highlights the column reference {anchorTerm QueryOops1}`c! "location"`:
@@ -804,12 +851,21 @@ Unfortunately, it is beyond the scope of this book to provide a description of i
 An indexed family such as {anchorName Query}`Query` is probably best as the core of a typed database interaction library, rather than its user interface.
 
 # Exercises
+%%%
+tag := "typed-query-exercises"
+%%%
 
 ## Dates
+%%%
+tag := none
+%%%
 
 Define a structure to represent dates. Add it to the {anchorName DBExpr}`DBType` universe and update the rest of the code accordingly. Provide the extra {anchorName DBExpr}`DBExpr` constructors that seem to be necessary.
 
 ## Nullable Types
+%%%
+tag := none
+%%%
 
 Add support for nullable columns to the query language by representing database types with the following structure:
 ```anchor nullable
@@ -827,6 +883,9 @@ abbrev NDBType.asType (t : NDBType) : Type :=
 Use this type in place of {anchorName DBExpr}`DBType` in {anchorName Schema}`Column` and {anchorName DBExpr}`DBExpr`, and look up SQL's rules for {lit}`NULL` and comparison operators to determine the types of {anchorName DBExpr}`DBExpr`'s constructors.
 
 ## Experimenting with Tactics
+%%%
+tag := none
+%%%
 
 
 What is the result of asking Lean to find values of the following types using {kw}`by repeat constructor`? Explain why each gives the result that it does.

diff --git a/book/FPLean/DependentTypes/UniversePattern.lean b/book/FPLean/DependentTypes/UniversePattern.lean
@@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples"
 set_option verso.exampleModule "Examples.DependentTypes.Finite"
 
 #doc (Manual) "The Universe Design Pattern" =>
+%%%
+tag := "universe-pattern"
+%%%
 
 In Lean, types such as {anchorTerm sundries}`Type`, {anchorTerm sundries}`Type 3`, and {anchorTerm sundries}`Prop` that classify other types are known as universes.
 However, the term _universe_ is also used for a design pattern in which a datatype is used to represent a subset of Lean's types, and a function converts the datatype's constructors into actual types.
@@ -90,6 +93,9 @@ Hint: Additional diagnostic information may be available using the `set_option d
 The {anchorName beqNoCases}`t` in the error message stands for an unknown value of type {anchorName beqNoCases}`NestedPairs`.
 
 # Type Classes vs Universes
+%%%
+tag := "type-classes-vs-universe-pattern"
+%%%
 
 Type classes allow an open-ended collection of types to be used with an API as long as they have implementations of the necessary interfaces.
 In most cases, this is preferable.
@@ -104,6 +110,9 @@ This is useful in a few situations:
 Type classes are useful in many of the same situations as interfaces in Java or C#, while a universe à la Tarski can be useful in cases where a sealed class might be used, but where an ordinary inductive datatype is not usable.
 
 # A Universe of Finite Types
+%%%
+tag := "finite-type-universe"
+%%%
 
 Restricting the types that can be used with an API to a predetermined collection can enable operations that would be impossible for an open-ended API.
 For example, functions can't normally be compared for equality.
@@ -350,6 +359,9 @@ Nested exponentials grow quickly, and there are many higher-order functions.
 
 
 # Exercises
+%%%
+tag := "universe-exercises"
+%%%
 
  * Write a function that converts any value from a type coded for by {anchorName Finite}`Finite` into a string. Functions should be represented as their tables.
  * Add the empty type {anchorName sundries}`Empty` to {anchorName Finite}`Finite` and {anchorName FiniteBeq}`Finite.beq`.