feat: link targets for redirects in old manual (#93)

Manual.lean

@@ -11,7 +11,7 @@ import Manual.Language
 import Manual.Terms
 import Manual.Tactics
 import Manual.Simp
-import Manual.BuiltInTypes
+import Manual.BasicTypes
 
 open Verso.Genre Manual
 
@@ -36,7 +36,11 @@ set_option pp.rawOnError true
 
 {include 0 Manual.Simp}
 
-{include 0 Manual.BuiltInTypes}
+{include 0 Manual.BasicTypes}
+
+# Standard Library
+
+## Optional Values
 
 # Notations and Macros
 %%%

Manual/BasicTypes.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+
+import Manual.Meta
+import Manual.BasicTypes.Nat
+import Manual.BasicTypes.String
+
+open Manual.FFIDocType
+
+open Verso.Genre Manual
+
+set_option pp.rawOnError true
+
+
+#doc (Manual) "Basic Types" =>
+
+Lean includes a number of built-in datatypes 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.
+
+{include 0 Manual.BasicTypes.Nat}
+
+# Integers
+
+# Fixed-Precision Integer Types
+
+# Floating-Point Numbers
+
+# Characters
+
+{docstring Char}
+
+## Syntax
+
+## Logical Model
+
+
+
+## Run-Time Representation
+
+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.
+
+
+## API Reference
+
+### Character Classes
+
+{docstring Char.isAlpha}
+
+{docstring Char.isAlphanum}
+
+{docstring Char.isDigit}
+
+{docstring Char.isLower}
+
+{docstring Char.isUpper}
+
+{docstring Char.isWhitespace}
+
+
+{include 0 Manual.BasicTypes.String}
+
+# Linked Lists
+
+# Arrays
+
+::: planned 91
+Description and API reference for {name}`Thunk`:
+ * Logical model as wrapper around a function from {lean}`Unit`
+ * Run-time realization as a lazy computation
+ * API reference
+:::
+
+
+# Lazy Computations
+
+::: planned 92
+Description and API reference for {name}`Thunk`:
+ * Logical model as wrapper around a function from {lean}`Unit`
+ * Run-time realization as a lazy computation
+ * API reference
+:::
+
+# Tasks and Threads
+
+::: planned 90
+Description and API reference for {name}`Task` and runtime threads, including {lean}`IO.Promise`
+
+ * Scheduling model
+ * Things to be careful of
+
+This section may be moved to the section on {name}`IO` in particular.
+:::

Manual/BuiltInTypes/String.lean → Manual/BasicTypes/String.lean

@@ -8,9 +8,9 @@ import VersoManual
 
 import Manual.Meta
 
-import Manual.BuiltInTypes.String.Logical
-import Manual.BuiltInTypes.String.Literals
-import Manual.BuiltInTypes.String.FFI
+import Manual.BasicTypes.String.Logical
+import Manual.BasicTypes.String.Literals
+import Manual.BasicTypes.String.FFI
 
 open Manual.FFIDocType
 
@@ -32,7 +32,7 @@ The fact that strings are internally represented as UTF-8-encoded byte arrays is
  * There is no operation to project a particular character out of the string, as this would be a performance trap. {ref "string-iterators"}[Use a {name}`String.Iterator`] in a loop instead of a {name}`Nat`.
  * Strings are indexed by {name}`String.Pos`, which internally records _byte counts_ rather than _character counts_, and thus takes constant time. Aside from `0`, these should not be constructed directly, but rather updated using {name}`String.next` and {name}`String.prev`.
 
-{include 0 Manual.BuiltInTypes.String.Logical}
+{include 0 Manual.BasicTypes.String.Logical}
 
 # Run-Time Representation
 %%%
@@ -72,7 +72,7 @@ Otherwise, a new string must be allocated.
 Despite the fact that they appear to be an ordinary constructor and projection, {name}`String.mk` and {name}`String.data` take *time linear in the length of the string*.
 This is because they must implement the conversions between lists of characters and packed arrays of bytes, which must necessarily visit each character.
 
-{include 0 Manual.BuiltInTypes.String.Literals}
+{include 0 Manual.BasicTypes.String.Literals}
 
 # API Reference
 
@@ -367,4 +367,4 @@ TODO Substring API xref
 {docstring String.crlfToLf}
 
 
-{include 0 Manual.BuiltInTypes.String.FFI}
+{include 0 Manual.BasicTypes.String.FFI}