Update Documentation to use new expression terminology (#5890)

# Changes

## Terminology Updates
This PR updates documentation to align with the expression phase
terminology changes introduced in
[#2964](#2964):

* **"symbolic value" → "symbolic constant"**: Updated all remaining
instances using find-and-replace

## Scope of Changes
* Focused on documentation that predates the July 2023 terminology
change
* Used git blame history to identify instances likely using the old
"constant" definition
* Manually reviewed each "constant" usage to distinguish between:
- New definition (unchanged): the broader category including symbolic
constants

Closes
[#5599](#5599)

---------

Co-authored-by: Hitesh Joshi <[email protected]>

Author: evoxtorm

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._

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

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 {}
 

toolchain/check/type_structure.h

@@ -166,7 +166,7 @@ class TypeStructure : public Printable<TypeStructure> {
       llvm::SmallVector<ConcreteType>::const_iterator& lhs_concrete_cursor,
       llvm::SmallVector<Structural>::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<Structural> structure_;
 
   // Indices of the symbolic entries in structure_.
@@ -179,7 +179,7 @@ class TypeStructure : public Printable<TypeStructure> {
 
 // 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`.