Update Documentation to use new expression terminology

docs/design/classes.md

@@ -1098,7 +1098,7 @@ class, but other kinds of type declarations, like choice types, are allowed.
 
 ### Let
 
-Other type constants can be defined using a `let` declaration:
+Other type template constants can be defined using a `let` declaration:
 
 ```
 class MyClass {
@@ -1107,8 +1107,8 @@ class MyClass {
 }
 ```
 
-The `:!` indicates that this is defining a compile-time constant, and so does
-not affect the storage of instances of that class.
+The `:!` indicates that this is defining a compile-time template constant, and
+so does not affect the storage of instances of that class.
 
 ### Alias
 

docs/design/expressions/bitwise.md

@@ -151,43 +151,43 @@ here.
 
 ## Integer constants
 
-These operations can also be applied to a pair of integer constants, or to an
-integer constant and a value of integer type, as follows:
+These operations can also be applied to a pair of integer template constants, or
+to an integer template constant and a value of integer type, as follows:
 
 -   If any binary bitwise or bit-shift operator is applied to two integer
-    constants, or the unary `^` operator is applied to an integer constant, the
-    result is an integer constant. Integer constants are treated as having
-    infinitely many high-order bits, where all but finitely many of those bits
-    are sign bits. For example, `-1` comprises infinitely many `1` bits. Note
-    that there is no difference between an arithmetic and a logical right shift
-    on an integer constant, because every bit always has a higher-order bit to
-    shift from.
+    constants, or the unary `^` operator is applied to an integer template
+    constant, the result is an integer template constant. Integer template
+    constants are treated as having infinitely many high-order bits, where all
+    but finitely many of those bits are sign bits. For example, `-1` comprises
+    infinitely many `1` bits. Note that there is no difference between an
+    arithmetic and a logical right shift on an integer template constant,
+    because every bit always has a higher-order bit to shift from.
     -   It is easy to produce extremely large numbers by left-shifting an
-        integer constant. For example, the binary representation of
+        integer template constant. For example, the binary representation of
         `1 << (1 << 1000)` is thought to be substantially larger than the total
         entropy in the observable universe. In practice, Carbon implementations
-        will set a much lower limit on the largest integer constant that they
-        support.
+        will set a much lower limit on the largest integer template constant
+        that they support.
 -   If a binary bitwise `&`, `|`, or `^` operation is applied to an integer
-    constant and a value of an integer type to which the constant can be
-    implicitly converted, the operand that is an integer constant is implicitly
-    converted to the integer type and the computation is performed as described
-    [above](#integer-types).
--   If the second operand of a bit-shift operator is an integer constant and the
-    first operand is not, and the second operand is between 0 (inclusive) and
-    the bit-width of the first operand (exclusive), the integer constant is
-    converted to an integer type that can hold its value and the computation is
-    performed as described above.
-
-Other operations involving integer constants are invalid. For example, a bitwise
-`&` between a `u8` and an integer constant `500` is invalid because `500`
-doesn't fit into `u8`, and `1 << n` is invalid if `n` is an integer variable
-because we don't know what type to use to compute the result.
-
-Note that the unary `^` operator applied to a non-negative integer constant
-results in a negative integer constant, and the binary `^` operator gives a
-negative result if exactly one of the input operands was negative. For example,
-`^0 == -1` evaluates to `true`.
+    template constant and a value of an integer type to which the constant can
+    be implicitly converted, the operand that is an integer template constant is
+    implicitly converted to the integer type and the computation is performed as
+    described [above](#integer-types).
+-   If the second operand of a bit-shift operator is an integer template
+    constant and the first operand is not, and the second operand is between 0
+    (inclusive) and the bit-width of the first operand (exclusive), the integer
+    template constant is converted to an integer type that can hold its value
+    and the computation is performed as described above.
+
+Other operations involving integer template constants are invalid. For example,
+a bitwise `&` between a `u8` and an integer template constant `500` is invalid
+because `500` doesn't fit into `u8`, and `1 << n` is invalid if `n` is an
+integer variable because we don't know what type to use to compute the result.
+
+Note that the unary `^` operator applied to a non-negative integer template
+constant results in a negative integer template constant, and the binary `^`
+operator gives a negative result if exactly one of the input operands was
+negative. For example, `^0 == -1` evaluates to `true`.
 
 ## Extensibility
 

docs/design/expressions/comparison_operators.md

@@ -220,15 +220,16 @@ wider type than either of the operand types.
 
 We permit the following comparisons involving constants:
 
--   A constant can be compared with a value of any type to which it can be
-    implicitly converted.
--   Any two constants can be compared, even if there is no type that can
-    represent both.
+-   A template constant can be compared with a value of any type to which it can
+    be implicitly converted.
+-   Any two template constants can be compared, even if there is no type that
+    can represent both.
 
 As described in [implicit conversions](implicit_conversions.md#data-types),
-integer constants can be implicitly converted to any integer or floating-point
-type that can represent their value, and floating-point constants can be
-implicitly converted to any floating-point type that can represent their value.
+integer template constants can be implicitly converted to any integer or
+floating-point type that can represent their value, and floating-point template
+constants can be implicitly converted to any floating-point type that can
+represent their value.
 
 Note that this disallows comparisons between, for example, `i32` and an integer
 literal that cannot be represented in `i32`. Such comparisons would always be

docs/design/expressions/implicit_conversions.md

@@ -116,12 +116,13 @@ The following implicit numeric conversions are available:
 In each case, the numerical value is the same before and after the conversion.
 An integer zero is translated into a floating-point positive zero.
 
-An integer constant can be implicitly converted to any type `iM`, `uM`, or `fM`
-in which that value can be exactly represented. A floating-point constant can be
-implicitly converted to any type `fM` in which that value is between the least
-representable finite value and the greatest representable finite value
-(inclusive), and converts to the nearest representable finite value, with ties
-broken by picking the value for which the mantissa is even.
+An integer template constant can be implicitly converted to any type `iM`, `uM`,
+or `fM` in which that value can be exactly represented. A floating-point
+template constant can be implicitly converted to any type `fM` in which that
+value is between the least representable finite value and the greatest
+representable finite value (inclusive), and converts to the nearest
+representable finite value, with ties broken by picking the value for which the
+mantissa is even.
 
 The above conversions are also precisely those that C++ considers non-narrowing,
 except:
@@ -131,16 +132,17 @@ except:
     converted to `f64`. Lossy conversions, such as from `i32` to `f32`, are not
     permitted.
 
--   What Carbon considers to be an integer constant or floating-point constant
-    may differ from what C++ considers to be a constant expression.
+-   What Carbon considers to be an integer template constant or floating-point
+    template constant may differ from what C++ considers to be a template
+    constant expression.
 
-    **Note:** We have not yet decided what will qualify as a constant in this
-    context, but it will include at least integer and floating-point literals,
-    with optional enclosing parentheses. It is possible that such constants will
-    have singleton types; see issue
+    **Note:** We have not yet decided what will qualify as a template constant
+    in this context, but it will include at least integer and floating-point
+    literals, with optional enclosing parentheses. It is possible that such
+    template constants will have singleton types; see issue
     [#508](https://github.com/carbon-language/carbon-lang/issues/508).
 
-In addition to the above rules, a negative integer constant `k` can be
+In addition to the above rules, a negative integer template constant `k` can be
 implicitly converted to the type `uN` if the value `k` + 2<sup>N</sup> can be
 exactly represented, and converts to that value. Note that this conversion
 violates the "semantics-preserving" test. For example, `(-1 as u8) as i32`

docs/design/expressions/member_access.md

@@ -335,7 +335,7 @@ generic parameter, or in fact any
 [compile-time binding](/docs/design/generics/terminology.md#bindings), the
 lookup is performed from a context where the value of that binding is unknown.
 Evaluation of an expression involving the binding may still succeed, but will
-result in a symbolic value involving that binding.
+result in a symbolic constant involving that binding.
 
 ```carbon
 class GenericWrapper(T:! type) {

docs/design/generics/appendix-rewrite-constraints.md

@@ -363,7 +363,7 @@ fn F[T:! C](x: T) {
 ```
 
 When looking up the name `N`, if `C` is an interface `I` and `N` is the name of
-an associated constant in that interface, the result is a symbolic value
+an associated constant in that interface, the result is a symbolic constant
 representing "the member `N` of `I`". If `C` is formed by combining interfaces
 with `&`, all such results are required to find the same associated constant,
 otherwise we reject for ambiguity.
@@ -439,7 +439,7 @@ is discussed later.
 ### Type substitution
 
 At various points during the type-checking of a Carbon program, we need to
-substitute a set of (binding, value) pairs into a symbolic value. We saw an
+substitute a set of (binding, value) pairs into a symbolic constant. We saw an
 example above: substituting `Self = W` into the type `A where .(A.T) = Self.U`
 to produce the value `A where .(A.T) = W.U`. Another important case is the
 substitution of inferred parameter values into the type of a function when
@@ -504,14 +504,14 @@ fn J[V:! A where .T = K](y: V) {
 }
 ```
 
-The values being substituted into the symbolic value are themselves already
+The values being substituted into the symbolic constant are themselves already
 fully substituted and resolved, and in particular, satisfy property 1 given
 above.
 
-Substitution proceeds by recursively rebuilding each symbolic value, bottom-up,
-replacing each substituted binding with its value. Doing this naively will
-propagate values like `i32` in the `F`/`G` case earlier in this section, but
-will not propagate rewrite constants like in the `H`/`J` case. The reason is
+Substitution proceeds by recursively rebuilding each symbolic constant,
+bottom-up, replacing each substituted binding with its value. Doing this naively
+will propagate values like `i32` in the `F`/`G` case earlier in this section,
+but will not propagate rewrite constants like in the `H`/`J` case. The reason is
 that the `.T = K` constraint is in the _type_ of the substituted value, rather
 than in the substituted value itself: deducing `T = i32` and converting `i32` to
 the type `C` of `T` preserves the value `i32`, but deducing `U = V` and

docs/design/generics/details.md

@@ -775,7 +775,7 @@ checked-generic function.
 
 A checked-generic caller of a checked-generic function performs the same
 substitution process to determine the return type, but the result may be a
-symbolic value. In this example of calling a checked generic from another
+symbolic constant. In this example of calling a checked generic from another
 checked generic,
 
 ```carbon

docs/design/generics/overview.md

@@ -373,7 +373,7 @@ kind of parameter is defined using a different syntax: a checked parameter is
 uses a symbolic binding pattern, a template parameter uses a template binding
 pattern, and a regular parameter uses a runtime binding pattern. Likewise, it's
 allowed to pass a symbolic or template constant value to a checked or regular
-parameter. _We have decided to support passing a symbolic value to a template
+parameter. _We have decided to support passing a symbolic constant to a template
 parameter, see
 [leads issue #2153: Checked generics calling templates](https://github.com/carbon-language/carbon-lang/issues/2153),
 but incorporating it into the design is future work._

proposals/p0851.md

@@ -269,10 +269,10 @@ answer for now.
 ### Inferring a variable type from literals
 
 Using the type on the right side for `var y: auto = 1` currently results in a
-constant `IntLiteral` value, whereas most languages would suggest a variable
-integer value. This is something that will be considered as part of type
-inference in general, because it also affects generics, templates, lambdas, and
-return types.
+template constant `IntLiteral` value, whereas most languages would suggest a
+variable integer value. This is something that will be considered as part of
+type inference in general, because it also affects generics, templates, lambdas,
+and return types.
 
 ## Rationale based on Carbon's goals
 

proposals/p2173.md

@@ -582,7 +582,7 @@ fn F[T:! C](x: T) {
 ```
 
 When looking up the name `N`, if `C` is an interface `I` and `N` is the name of
-an associated constant in that interface, the result is a symbolic value
+an associated constant in that interface, the result is a symbolic constant
 representing "the member `N` of `I`". If `C` is formed by combining interfaces
 with `&`, all such results are required to find the same associated constant,
 otherwise we reject for ambiguity.
@@ -660,7 +660,7 @@ is discussed later.
 #### Type substitution
 
 At various points during the type-checking of a Carbon program, we need to
-substitute a set of (binding, value) pairs into a symbolic value. We saw an
+substitute a set of (binding, value) pairs into a symbolic constant. We saw an
 example above: substituting `Self = T` into the type `A where .(A.T) = Self.U`
 to produce the value `A where .(A.T) = T.U`. Another important case is the
 substitution of inferred parameter values into the type of a function when
@@ -725,14 +725,14 @@ fn J[V:! A where .T = K](y: V) {
 }
 ```
 
-The values being substituted into the symbolic value are themselves already
+The values being substituted into the symbolic constant are themselves already
 fully substituted and resolved, and in particular, satisfy property 1 given
 above.
 
-Substitution proceeds by recursively rebuilding each symbolic value, bottom-up,
-replacing each substituted binding with its value. Doing this naively will
-propagate values like `i32` in the `F`/`G` case earlier in this section, but
-will not propagate rewrite constants like in the `H`/`J` case. The reason is
+Substitution proceeds by recursively rebuilding each symbolic constant,
+bottom-up, replacing each substituted binding with its value. Doing this naively
+will propagate values like `i32` in the `F`/`G` case earlier in this section,
+but will not propagate rewrite constants like in the `H`/`J` case. The reason is
 that the `.T = K` constraint is in the _type_ of the substituted value, rather
 than in the substituted value itself: deducing `T = i32` and converting `i32` to
 the type `C` of `T` preserves the value `i32`, but deducing `U = V` and

proposals/p2200.md

@@ -235,7 +235,7 @@ Template generic bindings are declared using the `template` keyword in addition
 to the `:!` of all generic bindings. This includes `let` declarations, as in:
 
 ```carbon
-// `N` is a constant that may be used in types.
+// `N` is a template constant that may be used in types.
 let template N:! i64 = 4;
 var my_array: [u8; N] = (255, 128, 64, 255);
 ```
@@ -261,7 +261,7 @@ context to produce r-values, not in a `var` context to produce l-values.
 
 ```carbon
 // ❌ Error: Can't use `:!` with `var`. Can't be both a
-//           compile-time constant and a variable.
+//           compile-time template constant and a variable.
 var N:! i64 = 4;
 // ❌ Error: Can't use `template :!` with `var` for the
 //           same reason.
@@ -282,9 +282,9 @@ R-values are divided into three different _value phases_:
 -   A _constant_ has a value known at compile time, and that value is available
     during type checking, for example to use as the size of an array. These
     include literals (integer, floating-point, string), concrete type values
-    (like `f64` or `Optional(i32*)`), expressions in terms of constants, and
-    values of `template` parameters.
--   A _symbolic value_ has a value that will be known at the code generation
+    (like `f64` or `Optional(i32*)`), expressions in terms of template
+    constants, and values of `template` parameters.
+-   A _symbolic constant_ has a value that will be known at the code generation
     stage of compilation when monomorphization happens, but is not known during
     type checking. This includes checked-generic parameters, and type
     expressions with checked-generic arguments, like `Optional(T*)`.
@@ -293,9 +293,9 @@ R-values are divided into three different _value phases_:
 So:
 
 -   A `let template T:! ...` or `fn F(template T:! ...)` declaration binds `T`
-    with constant value phase,
--   A `let T:! ...` or `fn F(T:! ...)` declaration binds `T` with symbolic value
-    phase,
+    with template constant value phase,
+-   A `let T:! ...` or `fn F(T:! ...)` declaration binds `T` with symbolic
+    constant phase,
 -   A `let x: ...` or `fn F(x: ...)` declaration binds `x` with runtime value
     phase.
 
@@ -319,9 +319,10 @@ considered in question-for-leads issue
 in addition to
 [#1371: Is `let` referentially transparent?](https://github.com/carbon-language/carbon-lang/issues/1371).
 
-**Note:** Exactly which expressions in terms of constants result in constants is
-an open question that is not resolved by this proposal. In particular, which
-function calls will be evaluated at compile time is not yet specified. See
+**Note:** Exactly which expressions in terms of template constants result in
+template constants is an open question that is not resolved by this proposal. In
+particular, which function calls will be evaluated at compile time is not yet
+specified. See
 [future work](#which-expressions-will-be-evaluated-at-compile-time).
 
 ### `auto`
@@ -1002,17 +1003,18 @@ class Vector(template T:! Type) {
 ### Value phase of bindings determined by initializer
 
 We considered allowing a `let` binding to result in a name with
-[constant value phase](#value-phases) if the initializer was a constant, even if
-it was not declared using the `template` keyword. That would mean that
-`let x: i32 = 5;` would declare `x` as constant, rather than a runtime value.
+[constant value phase](#value-phases) if the initializer was a template
+constant, even if it was not declared using the `template` keyword. That would
+mean that `let x: i32 = 5;` would declare `x` as template constant, rather than
+a runtime value.
 
 For non-type values, this would be a strict improvement in usability. With the
 proposal, there is a choice between writing the concise form `let x: i32 = 5;`
 and `let template x:! i32 = 5;` that lets the compiler use the value of `x`
 directly. The `let template` form is both longer and uses `template` which in
 other contexts might merit closer scrutiny, but is generally either desirable or
 harmless in this context. The problem is that for type values, changing from a
-symbolic value to a constant results in a change to the
+symbolic constant to a template constant results in a change to the
 [name lookup](#name-lookup) rules, which is not going to always be desired.
 
 This decision was the result of a discussion in open discussions on