diff --git a/docs/design/expressions/bitwise.md b/docs/design/expressions/bitwise.md
index 3fe19cf509dfc..5d989a83fecee 100644
--- a/docs/design/expressions/bitwise.md
+++ b/docs/design/expressions/bitwise.md
@@ -13,7 +13,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
- [Overview](#overview)
- [Precedence and associativity](#precedence-and-associativity)
- [Integer types](#integer-types)
-- [Integer constants](#integer-constants)
+- [Integer template constants](#integer-template-constants)
- [Extensibility](#extensibility)
- [Alternatives considered](#alternatives-considered)
- [References](#references)
@@ -149,45 +149,45 @@ second operand is not within that range.
arithmetic overflow, document the behavior in a common place and link to it from
here.
-## Integer constants
+## Integer template 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:
+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
diff --git a/docs/design/expressions/comparison_operators.md b/docs/design/expressions/comparison_operators.md
index 262264ad5e2fa..9edd999db3f45 100644
--- a/docs/design/expressions/comparison_operators.md
+++ b/docs/design/expressions/comparison_operators.md
@@ -222,13 +222,14 @@ 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.
+- 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
diff --git a/docs/design/expressions/implicit_conversions.md b/docs/design/expressions/implicit_conversions.md
index ec8e1fdeed0f6..87ea799f0e16d 100644
--- a/docs/design/expressions/implicit_conversions.md
+++ b/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` + 2N 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`
diff --git a/docs/design/expressions/member_access.md b/docs/design/expressions/member_access.md
index f496376b71716..f6b49d60da361 100644
--- a/docs/design/expressions/member_access.md
+++ b/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) {
diff --git a/docs/design/generics/appendix-rewrite-constraints.md b/docs/design/generics/appendix-rewrite-constraints.md
index c6ef3f4d918c6..a68b8ba4725da 100644
--- a/docs/design/generics/appendix-rewrite-constraints.md
+++ b/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
diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md
index 64c2a977903fa..3a52d3cf78b15 100644
--- a/docs/design/generics/details.md
+++ b/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
diff --git a/docs/design/generics/overview.md b/docs/design/generics/overview.md
index 6979b683e6bbc..3054b27fe8f5f 100644
--- a/docs/design/generics/overview.md
+++ b/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._
diff --git a/toolchain/check/impl_lookup.h b/toolchain/check/impl_lookup.h
index 8323354a58af9..ecdb0d8720923 100644
--- a/toolchain/check/impl_lookup.h
+++ b/toolchain/check/impl_lookup.h
@@ -49,9 +49,10 @@ auto LookupMatchesImpl(Context& context, SemIR::LocId loc_id,
// The result of EvalLookupSingleImplWitness(). It can be one of:
// - No value. Lookup failed to find an impl declaration.
-// - A concrete value. Lookup found a concrete impl declaration that can be
+// - A template constant. Lookup found a concrete impl declaration that can be
// used definitively.
-// - A symbolic value. Lookup found an impl but it is not returned since lookup
+// - A symbolic value. Lookup found an impl but it is not returned since
+// lookup
// will need to be done again with a more specific query to look for
// specializations.
class [[nodiscard]] EvalImplLookupResult {
diff --git a/toolchain/check/testdata/deduce/symbolic_facets.carbon b/toolchain/check/testdata/deduce/symbolic_facets.carbon
index 346c4c001eea7..9327061566aec 100644
--- a/toolchain/check/testdata/deduce/symbolic_facets.carbon
+++ b/toolchain/check/testdata/deduce/symbolic_facets.carbon
@@ -12,7 +12,7 @@
// By placing each interface inside a generic class, a facet type refering to
// the interface becomes symbolic. Normally they would be concrete. This can
-// affect decisions in deduce which unwraps symbolic values, but still needs to
+// affect decisions in deduce which unwraps symbolic constants, but still needs to
// ensure they convert correctly.
// --- fail_missing_interface.carbon
diff --git a/toolchain/check/testdata/impl/lookup/symbolic_lookup.carbon b/toolchain/check/testdata/impl/lookup/symbolic_lookup.carbon
index cefdccf9ec4a6..b4e110f626782 100644
--- a/toolchain/check/testdata/impl/lookup/symbolic_lookup.carbon
+++ b/toolchain/check/testdata/impl/lookup/symbolic_lookup.carbon
@@ -59,7 +59,7 @@ interface Z(T:! type) {
let X:! type;
}
-// This impl has a rewrite to a symbolic value, and the `.Self` type has a
+// This impl has a rewrite to a symbolic constant, and the `.Self` type has a
// dependency on a generic parameter.
final impl forall [T:! type, S:! type] T as Z(S) where .X = T {}
diff --git a/toolchain/check/type_structure.h b/toolchain/check/type_structure.h
index 12821e239d504..a7c101e4894e1 100644
--- a/toolchain/check/type_structure.h
+++ b/toolchain/check/type_structure.h
@@ -163,7 +163,7 @@ class TypeStructure : public Printable {
llvm::SmallVector::const_iterator& lhs_concrete_cursor,
llvm::SmallVector::const_iterator& rhs_cursor) -> bool;
- // The structural position of concrete and symbolic values in the type.
+ // The structural position of concrete and symbolic constants in the type.
llvm::SmallVector structure_;
// Indices of the symbolic entries in structure_.
@@ -176,7 +176,7 @@ class TypeStructure : public Printable {
// Constructs the TypeStructure for a self type or facet value and an interface
// constraint (e.g. `Iface(A, B(C))`), which represents the location of unknown
-// symbolic values in the combined signature and which is ordered by them.
+// symbolic constants in the combined signature and which is ordered by them.
//
// Given `impl C as Z {}` the `self_const_id` would be a `C` and the interface
// constraint would be `Z`.