Replace keyword `is` with `impls` (#2483)

Use the keyword `impls` instead of `is` when writing a `where` constraint that a type variable needs to implement an interface or named constraint.

What was previously (provisionally) written:
```
fn Sort[T:! Container where .ElementType is Ordered](x: T*);
```
will now be written:
```
fn Sort[T:! Container where .ElementType impls Ordered](x: T*);
```

---------

Co-authored-by: Geoff Romer <gromer@google.com>
Co-authored-by: Chandler Carruth <chandlerc@gmail.com>

docs/design/README.md

@@ -2907,13 +2907,14 @@ pick which definition is selected. These rules ensure:
     if it can see an impl that applies, even though another more specific impl
     may be selected.
 
-Implementations may be marked [`final`](generics/details.md#final-impls) to
-indicate that they may not be specialized, subject to
-[some restrictions](generics/details.md#libraries-that-can-contain-final-impls).
+Implementations may be marked
+[`final`](generics/details.md#final-impl-declarations) to indicate that they may
+not be specialized, subject to
+[some restrictions](generics/details.md#libraries-that-can-contain-a-final-impl).
 
 > References:
 >
-> -   [Generic or parameterized impls](generics/details.md#parameterized-impls)
+> -   [Generic or parameterized impl declarationss](generics/details.md#parameterized-impl-declarations)
 > -   Proposal
 >     [#624: Coherence: terminology, rationale, alternatives considered](https://github.com/carbon-language/carbon-lang/pull/624)
 > -   Proposal
@@ -2988,7 +2989,7 @@ interfaces the compiler knows that a type implements. It is also possible that
 knowing a type implements one interface implies that it implements another, from
 an
 [interface requirement](generics/details.md#interface-requiring-other-interfaces)
-or [generic implementation](#generic-implementations). An `observe`...`is`
+or [generic implementation](#generic-implementations). An `observe`...`impls`
 declaration may be used to
 [observe that a type implements an interface](generics/details.md#observing-a-type-implements-an-interface).
 

docs/design/assignment.md

@@ -308,7 +308,7 @@ This defaulting is accomplished by a parameterized implementation of
 `OpAssignWith(U)` defined in terms of `AssignWith` and `OpWith`:
 
 ```
-impl forall [U:! type, T:! OpWith(U) where .Self is AssignWith(.Self.Result)]
+impl forall [U:! type, T:! OpWith(U) where .Self impls AssignWith(.Self.Result)]
     T as OpAssignWith(U) {
   fn Op[addr self: Self*](other: U) {
     // Here, `$` is the operator described by `OpWith`.

docs/design/classes.md

@@ -1168,7 +1168,7 @@ methods whose implementation may be overridden in a derived class.
 
 Only methods defined in the scope of the class definition may be virtual, not
 any defined in
-[external interface impls](/docs/design/generics/details.md#external-impl).
+[external interface `impl` declarations](/docs/design/generics/details.md#external-impl).
 Interface methods may be implemented using virtual methods when the
 [impl is internal](/docs/design/generics/details.md#implementing-interfaces),
 and calls to those methods by way of the interface will do virtual dispatch just

docs/design/expressions/comparison_operators.md

@@ -445,8 +445,8 @@ should have no observable side-effects.
     `a.Compare(b) == a.Compare(c)`.
 
 `OrderedWith` implementations should also be _consistent under reversal_. That
-is, given types `T` and `U` where `T is OrderedWith(U)` and
-`U is OrderedWith(T)`, and values `a: T` and `b: U`:
+is, given types `T` and `U` where `T impls OrderedWith(U)` and
+`U impls OrderedWith(T)`, and values `a: T` and `b: U`:
 
 -   If `a.(OrderedWith.Compare)(b)` is `Ordering.Greater`, then
     `b.(OrderedWith.Compare)(a)` is `Ordering.Less`, and the other way around.

docs/design/expressions/if.md

@@ -89,8 +89,8 @@ The interface `CommonTypeWith` is used to customize the behavior of
 ```
 interface CommonTypeWith(U:! type) {
   let Result:! type
-    where Self is ImplicitAs(.Self) and
-          U is ImplicitAs(.Self);
+    where Self impls ImplicitAs(.Self) and
+          U impls ImplicitAs(.Self);
 }
 ```
 
@@ -98,8 +98,8 @@ The implementation `A as CommonTypeWith(B)` specifies the type that `A` would
 like to result from unifying `A` and `B` as its `Result`.
 
 _Note:_ It is required that both types implicitly convert to the common type.
-Some blanket `impl`s for `CommonTypeWith` are provided as part of the prelude.
-These are described in the following sections.
+Some blanket `impl` declaractions for `CommonTypeWith` are provided as part of
+the prelude. These are described in the following sections.
 
 _Note:_ The same mechanism is expected to eventually be used to compute common
 types in other circumstances.
@@ -122,8 +122,8 @@ The interface `SymmetricCommonTypeWith` is an implementation detail of the
 ```
 interface SymmetricCommonTypeWith(U:! type) {
   let Result:! type
-    where Self is ImplicitAs(.Self) and
-          U is ImplicitAs(.Self);
+    where Self impls ImplicitAs(.Self) and
+          U impls ImplicitAs(.Self);
 }
 match_first {
   impl forall [T:! type, U:! CommonTypeWith(T)]
@@ -133,9 +133,10 @@ match_first {
 }
 ```
 
-The `SymmetricCommonTypeWith` interface is not exported, so user-defined `impl`s
-can't be defined, and only the two blanket `impl`s above are used. The
-`CommonType` constraint is then defined as follows:
+The `SymmetricCommonTypeWith` interface is not exported, so users may not
+declare their own implementations of it, and only the two blanket `impl`
+declarations above are used. The `CommonType` constraint is then defined as
+follows:
 
 ```
 constraint CommonType(U:! SymmetricCommonTypeWith(Self)) {
@@ -198,7 +199,7 @@ specific implementation exists, the constraints on `T as CommonType(U)` will not
 be met because `(T as CommonTypeWith(U)).Result` and
 `(U as CommonTypeWith(T)).Result` will differ. In order to define a common type
 for such a case, `CommonTypeWith` implementations in both directions must be
-provided to override the blanket `impl`s in both directions:
+provided to override the blanket `impl` declarations in both directions:
 
 ```
 impl MyString as CommonTypeWith(YourString) where .Result = MyString {}

docs/design/generics/details.md

@@ -70,19 +70,19 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Type compatible with another type](#type-compatible-with-another-type)
         -   [Same implementation restriction](#same-implementation-restriction)
         -   [Example: Multiple implementations of the same interface](#example-multiple-implementations-of-the-same-interface)
-        -   [Example: Creating an impl out of other impls](#example-creating-an-impl-out-of-other-impls)
+        -   [Example: Creating an impl out of other implementations](#example-creating-an-impl-out-of-other-implementations)
     -   [Sized types and type-of-types](#sized-types-and-type-of-types)
         -   [Implementation model](#implementation-model-2)
     -   [`TypeId`](#typeid)
     -   [Destructor constraints](#destructor-constraints)
 -   [Generic `let`](#generic-let)
--   [Parameterized impls](#parameterized-impls)
+-   [Parameterized impl declarations](#parameterized-impl-declarations)
     -   [Impl for a parameterized type](#impl-for-a-parameterized-type)
     -   [Conditional conformance](#conditional-conformance)
         -   [Conditional methods](#conditional-methods)
-    -   [Blanket impls](#blanket-impls)
-        -   [Difference between blanket impls and named constraints](#difference-between-blanket-impls-and-named-constraints)
-    -   [Wildcard impls](#wildcard-impls)
+    -   [Blanket impl declarations](#blanket-impl-declarations)
+        -   [Difference between a blanket impl and a named constraint](#difference-between-a-blanket-impl-and-a-named-constraint)
+    -   [Wildcard impl declarations](#wildcard-impl-declarations)
     -   [Combinations](#combinations)
     -   [Lookup resolution and specialization](#lookup-resolution-and-specialization)
         -   [Type structure of an impl declaration](#type-structure-of-an-impl-declaration)
@@ -91,8 +91,8 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
         -   [Prioritization rule](#prioritization-rule)
         -   [Acyclic rule](#acyclic-rule)
         -   [Termination rule](#termination-rule)
-    -   [`final` impls](#final-impls)
-        -   [Libraries that can contain `final` impls](#libraries-that-can-contain-final-impls)
+    -   [`final` impl declarations](#final-impl-declarations)
+        -   [Libraries that can contain a `final` impl](#libraries-that-can-contain-a-final-impl)
     -   [Comparison to Rust](#comparison-to-rust)
 -   [Forward declarations and cyclic references](#forward-declarations-and-cyclic-references)
     -   [Declaring interfaces and named constraints](#declaring-interfaces-and-named-constraints)
@@ -108,7 +108,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Requirements with `where` constraints](#requirements-with-where-constraints)
 -   [Observing a type implements an interface](#observing-a-type-implements-an-interface)
     -   [Observing interface requirements](#observing-interface-requirements)
-    -   [Observing blanket impls](#observing-blanket-impls)
+    -   [Observing blanket impl declarations](#observing-blanket-impl-declarations)
 -   [Operator overloading](#operator-overloading)
     -   [Binary operators](#binary-operators)
     -   [`like` operator for implicit conversions](#like-operator-for-implicit-conversions)
@@ -121,7 +121,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Abstract return types](#abstract-return-types)
     -   [Evolution](#evolution)
     -   [Testing](#testing)
-    -   [Impls with state](#impls-with-state)
+    -   [Impl with state](#impl-with-state)
     -   [Generic associated types and higher-ranked types](#generic-associated-types-and-higher-ranked-types)
         -   [Generic associated types](#generic-associated-types)
         -   [Higher-ranked types](#higher-ranked-types)
@@ -245,14 +245,14 @@ definitions for all the functions (and other members) declared in the interface.
 
 Carbon interfaces are ["nominal"](terminology.md#nominal-interfaces), which
 means that types explicitly describe how they implement interfaces. An
-["impl"](terminology.md#impls-implementations-of-interfaces) defines how one
+["impl"](terminology.md#impl-implementation-of-an-interface) defines how one
 interface is implemented for a type. Every associated entity is given a
 definition. Different types satisfying `Vector` can have different definitions
 for `Add` and `Scale`, so we say their definitions are _associated_ with what
 type is implementing `Vector`. The `impl` defines what is associated with the
 type for that interface.
 
-Impls may be defined inline inside the type definition:
+An impl may be defined inline inside the type definition:
 
 ```
 class Point {
@@ -421,8 +421,8 @@ interface (`Vector` in this case) in addition to the library that defines the
 type (`Point3` here). This (at least partially) addresses
 [the expression problem](https://eli.thegreenplace.net/2016/the-expression-problem-and-its-solutions).
 
-Carbon requires `impl`s defined in a different library to be `external` so that
-the API of `Point3` doesn't change based on what is imported. It would be
+Carbon requires `impl` declarations in a different library to be `external` so
+that the API of `Point3` doesn't change based on what is imported. It would be
 particularly bad if two different libraries implemented interfaces with
 conflicting names that both affected the API of a single type. As a consequence
 of this restriction, you can find all the names of direct members (those
@@ -731,7 +731,7 @@ A possible model for generating code for a generic function is to use a
 implements an interface:
 
 -   [Interfaces](#interfaces) are types of witness tables.
--   [Impls](#implementing-interfaces) are witness table values.
+-   An [impl](#implementing-interfaces) is a witness table value.
 
 Type checking is done with just the interface. The impl is used during code
 generation time, possibly using
@@ -2358,7 +2358,8 @@ class Bijection(FromType:! type, ToType:! type) {
   impl as Map(FromType, ToType) { ... }
   impl as Map(ToType, FromType) { ... }
 }
-// ❌ Error: Bijection has two impls of interface Map(String, String)
+// ❌ Error: Bijection has twodifferent impl definitions of
+// interface Map(String, String)
 var oops: Bijection(String, String) = ...;
 ```
 
@@ -2682,7 +2683,7 @@ since it can be applied to associated type members as well.
 In the following example, normally the `ElementType` of a `Container` can be any
 type. The `SortContainer` function, however, takes a pointer to a type
 satisfying `Container` with the additional constraint that its `ElementType`
-must satisfy the `Comparable` interface.
+must satisfy the `Comparable` interface, using an `impls` constraint:
 
 ```
 interface Container {
@@ -2691,7 +2692,7 @@ interface Container {
 }
 
 fn SortContainer
-    [ContainerType:! Container where .ElementType is Comparable]
+    [ContainerType:! Container where .ElementType impls Comparable]
     (container_to_sort: ContainerType*);
 ```
 
@@ -2699,13 +2700,9 @@ In contrast to [a same type constraint](#same-type-constraints), this does not
 say what type `ElementType` exactly is, just that it must satisfy some
 type-of-type.
 
-**Open question:** How do you spell that? Provisionally we are writing `is`,
-following Swift, but maybe we should have another operator that more clearly
-returns a boolean like `has_type`?
-
 **Note:** `Container` defines `ElementType` as having type `type`, but
 `ContainerType.ElementType` has type `Comparable`. This is because
-`ContainerType` has type `Container where .ElementType is Comparable`, not
+`ContainerType` has type `Container where .ElementType impls Comparable`, not
 `Container`. This means we need to be a bit careful when talking about the type
 of `ContainerType` when there is a `where` clause modifying it.
 
@@ -2731,7 +2728,7 @@ We can then define a function that only accepts types that implement
 
 ```
 fn F[ContainerType:! ContainerInterface
-     where .IteratorType is RandomAccessIterator]
+     where .IteratorType impls RandomAccessIterator]
     (c: ContainerType);
 ```
 
@@ -2741,18 +2738,18 @@ We would like to be able to name this constraint, defining a
 
 ```
 let RandomAccessContainer:! auto =
-    ContainerInterface where .IteratorType is RandomAccessIterator;
+    ContainerInterface where .IteratorType impls RandomAccessIterator;
 // or
 constraint RandomAccessContainer {
   extends ContainerInterface
-      where .IteratorType is RandomAccessIterator;
+      where .IteratorType impls RandomAccessIterator;
 }
 
 // With the above definition:
 fn F[ContainerType:! RandomAccessContainer](c: ContainerType);
 // is equivalent to:
 fn F[ContainerType:! ContainerInterface
-     where .IteratorType is RandomAccessIterator]
+     where .IteratorType impls RandomAccessIterator]
     (c: ContainerType);
 ```
 
@@ -2765,7 +2762,7 @@ and satisfy an interface:
 ```
 fn EqualContainers
     [CT1:! Container,
-     CT2:! Container where .ElementType is HasEquality
+     CT2:! Container where .ElementType impls HasEquality
                        and .ElementType == CT1.ElementType]
     (c1: CT1*, c2: CT2*) -> bool;
 ```
@@ -2870,7 +2867,7 @@ it is an error if `.Self` could mean two different things, as in:
 
 ```
 // ❌ Illegal: `.Self` could mean `T` or `T.A`.
-fn F[T:! InterfaceA where .A is
+fn F[T:! InterfaceA where .A impls
            (InterfaceB where .B == .Self)](x: T);
 ```
 
@@ -2889,7 +2886,7 @@ external impl Vector(String) as Printable { ... }
 
 // Constraint: `T` such that `Vector(T)` implements `Printable`
 fn PrintThree
-    [T:! type where Vector(.Self) is Printable]
+    [T:! type where Vector(.Self) impls Printable]
     (a: T, b: T, c: T) {
   var v: Vector(T) = (a, b, c);
   Print(v);
@@ -2903,16 +2900,16 @@ fn PrintThree
 
 In this case, we need some other type to implement an interface parameterized by
 a generic type parameter. The syntax for this case follows the previous case,
-except now the `.Self` parameter is on the interface to the right of the `is`.
-For example, we might need a type parameter `T` to support explicit conversion
-from an integer type like `i32`:
+except now the `.Self` parameter is on the interface to the right of the
+`impls`. For example, we might need a type parameter `T` to support explicit
+conversion from an integer type like `i32`:
 
 ```
 interface As(T:! type) {
   fn Convert[self: Self]() -> T;
 }
 
-fn Double[T:! Mul where i32 is As(.Self)](x: T) -> T {
+fn Double[T:! Mul where i32 impls As(.Self)](x: T) -> T {
   return x * (2 as T);
 }
 ```
@@ -2925,8 +2922,8 @@ current type. This means referring to some
 `.MemberName`, or [`.Self`](#recursive-constraints). Examples:
 
 -   `Container where .ElementType = i32`
--   `type where Vector(.Self) is Sortable`
--   `Addable where i32 is AddableWith(.Result)`
+-   `type where Vector(.Self) impls Sortable`
+-   `Addable where i32 impls AddableWith(.Result)`
 
 Constraints that only refer to other types should be moved to the type that is
 declared last. So:
@@ -2946,10 +2943,10 @@ fn F[A:! type, B:! type where A == .Self, C:! type](a: A, b: B, c: C);
 This includes `where` clauses used in an `impl` declaration:
 
 ```
-// ❌ Error: `where T is B` does not use `.Self` or a designator
-external impl forall [T:! type] T as A where T is B {}
+// ❌ Error: `where T impls B` does not use `.Self` or a designator
+external impl forall [T:! type] T as A where T impls B {}
 // ✅ Allowed
-external impl forall [T:! type where .Self is B] T as A {}
+external impl forall [T:! type where .Self impls B] T as A {}
 // ✅ Allowed
 external impl forall [T:! B] T as A {}
 ```
@@ -2991,13 +2988,13 @@ Effectively that means that these functions are automatically rewritten to add a
 ```
 fn LookUp[KeyType:! type]
     (hm: HashMap(KeyType, i32)*
-        where KeyType is Hashable & EqualityComparable & Movable,
+        where KeyType impls Hashable & EqualityComparable & Movable,
      k: KeyType) -> i32;
 
 fn PrintValueOrDefault[KeyType:! Printable,
                        ValueT:! Printable & HasDefault]
     (map: HashMap(KeyType, ValueT)
-        where KeyType is Hashable & EqualityComparable & Movable,
+        where KeyType impls Hashable & EqualityComparable & Movable,
      key: KeyT);
 ```
 
@@ -3064,7 +3061,7 @@ them, needs them to be `Hashable` and so on. To say "`T` is a type where
 `HashSet(T)` is legal," we can write:
 
 ```
-fn NumDistinct[T:! type where HashSet(.Self) is type]
+fn NumDistinct[T:! type where HashSet(.Self) impls type]
     (a: T, b: T, c: T) -> i32 {
   var set: HashSet(T);
   set.Add(a);
@@ -3326,7 +3323,7 @@ interfaces to generic types, they may be added without breaking existing code.
 
 There are some constraints that we will naturally represent as named
 type-of-types. These can either be used directly to constrain a generic type
-parameter, or in a `where ... is ...` clause to constrain an associated type.
+parameter, or in a `where ... impls ...` clause to constrain an associated type.
 
 The compiler determines which types implement these interfaces, developers can
 not explicitly implement these interfaces for their own types.
@@ -3341,7 +3338,7 @@ subtypes of `T`.
 
 ```
 fn F[T:! Extends(BaseType)](p: T*);
-fn UpCast[T:! type](p: T*, U:! type where T is Extends(.Self)) -> U*;
+fn UpCast[T:! type](p: T*, U:! type where T impls Extends(.Self)) -> U*;
 fn DownCast[T:! type](p: T*, U:! Extends(T)) -> U*;
 ```
 
@@ -3370,7 +3367,8 @@ have to include a "data representation requirement" option.
 
 `CompatibleWith` determines an equivalence relationship between types.
 Specifically, given two types `T1` and `T2`, they are equivalent if
-`T1 is CompatibleWith(T2)`. That is, if `T1` has the type `CompatibleWith(T2)`.
+`T1 impls CompatibleWith(T2)`. That is, if `T1` has the type
+`CompatibleWith(T2)`.
 
 **Note:** Just like interface parameters, we require the user to supply `U`,
 they may not be deduced. Specifically, this code would be illegal:
@@ -3402,7 +3400,7 @@ class HashSet(T:! Hashable) { ... }
 ```
 
 Then `HashSet(T)` may be cast to `HashSet(U)` if
-`T is CompatibleWith(U, Hashable)`. The one-parameter interpretation of
+`T impls CompatibleWith(U, Hashable)`. The one-parameter interpretation of
 `CompatibleWith(U)` is recovered by letting the default for the second `TT`
 parameter be `type`.
 
@@ -3463,7 +3461,7 @@ assert(CombinedCompare(Song(...), Song(...), (SongByArtist, SongByTitle)) ==
 through? They will also be needed for
 [variadic argument support](#variadic-arguments).
 
-#### Example: Creating an impl out of other impls
+#### Example: Creating an impl out of other implementations
 
 And then to package this functionality as an implementation of `Comparable`, we
 combine `CompatibleWith` with [type adaptation](#adapting-types):
@@ -3679,7 +3677,7 @@ can be used to switch to the API of `C` when it is external, as an alternative
 to [using an adapter](#use-case-accessing-external-names), or to simplify
 inlining of a generic function while preserving semantics.
 
-## Parameterized impls
+## Parameterized impl declarations
 
 There are cases where an impl definition should apply to more than a single type
 and interface combination. The solution is to parameterize the impl definition,
@@ -3690,11 +3688,11 @@ so it applies to a family of types, interfaces, or both. This includes:
 -   "Conditional conformance" where a parameterized type implements some
     interface if the parameter to the type satisfies some criteria, like
     implementing the same interface.
--   "Blanket" impls where an interface is implemented for all types that
-    implement another interface, or some other criteria beyond being a specific
-    type.
--   "Wildcard" impls where a family of interfaces are implemented for single
-    type.
+-   "Blanket" impl declarations where an interface is implemented for all types
+    that implement another interface, or some other criteria beyond being a
+    specific type.
+-   "Wildcard" impl declarations where a family of interfaces are implemented
+    for single type.
 
 ### Impl for a parameterized type
 
@@ -3720,8 +3718,8 @@ class Vector(T:! type) {
 ```
 
 An impl may be declared [external](#external-impl) by adding an `external`
-keyword before `impl`. External impls may also be declared out-of-line, but all
-parameters must be declared in a `forall` clause:
+keyword before `impl`. External impl declarations may also be out-of-line, but
+all parameters must be declared in a `forall` clause:
 
 ```
 external impl forall [T:! type] Vector(T) as Iterable
@@ -3787,8 +3785,8 @@ external impl forall [T:! Printable] Vector(T) as Printable {
 }
 ```
 
-To define these `impl`s inline in a `class` definition, include a `forall`
-clause with a more-specific type between the `impl` and `as` keywords.
+To include these `impl` definitions inline in a `class` definition, include a
+`forall` clause with a more-specific type between the `impl` and `as` keywords.
 
 ```
 class Array(T:! type, template N:! i64) {
@@ -3880,7 +3878,7 @@ a vector type that only has a `Sort` method if its elements implement the
 
 ```
 class Vector(T:! type) {
-  // `Vector(T)` has a `Sort()` method if `T` is `Comparable`.
+  // `Vector(T)` has a `Sort()` method if `T` impls `Comparable`.
   fn Sort[C:! Comparable, addr self: Vector(C)*]();
 }
 ```
@@ -3893,11 +3891,11 @@ methods using
 or
 [contextual where clauses](https://docs.swift.org/swift-book/LanguageGuide/Generics.html#ID628).
 
-### Blanket impls
+### Blanket impl declarations
 
-A _blanket impl_ is an `impl` that could apply to more than one root type, so
-the `impl` will use a type variable for the `Self` type. Here are some examples
-where blanket impls arise:
+A _blanket impl declaration_ is an `impl` declaration that could apply to more
+than one root type, so the `impl` declaration will use a type variable for the
+`Self` type. Here are some examples where blanket impl declarations arise:
 
 -   Any type implementing `Ordered` should get an implementation of
     `PartiallyOrdered`.
@@ -3915,15 +3913,15 @@ where blanket impls arise:
 
     This means that every type is the common type with itself.
 
-Blanket impls must always be [external](#external-impl) and defined lexically
-out-of-line.
+Blanket impl declarations must always be [external](#external-impl) and defined
+lexically out-of-line.
 
-#### Difference between blanket impls and named constraints
+#### Difference between a blanket impl and a named constraint
 
-A blanket interface can be used to say "any type implementing `interface I` also
-implements `interface B`." Compare this with defining a `constraint C` that
-requires `I`. In that case, `C` will also be implemented any time `I` is. There
-are differences though:
+A blanket impl declaration can be used to say "any type implementing
+`interface I` also implements `interface B`." Compare this with defining a
+`constraint C` that requires `I`. In that case, `C` will also be implemented any
+time `I` is. There are differences though:
 
 -   There can be other implementations of `interface B` without a corresponding
     implementation of `I`, unless `B` has a requirement on `I`. However, the
@@ -3931,12 +3929,13 @@ are differences though:
 -   More specialized implementations of `B` can override the blanket
     implementation.
 
-### Wildcard impls
+### Wildcard impl declarations
 
-A _wildcard impl_ is an impl that defines a family of interfaces for a single
-`Self` type. For example, the `BigInt` type might implement `AddTo(T)` for all
-`T` that implement `ImplicitAs(i32)`. The implementation would first convert `T`
-to `i32` and then add the `i32` to the `BigInt` value.
+A _wildcard impl declaration_ is an `impl` declaration that defines how a family
+of interfaces are implemented for a single `Self` type. For example, the
+`BigInt` type might implement `AddTo(T)` for all `T` that implement
+`ImplicitAs(i32)`. The implementation would first convert `T` to `i32` and then
+add the `i32` to the `BigInt` value.
 
 ```
 class BigInt {
@@ -3946,13 +3945,14 @@ class BigInt {
 external impl forall [T:! ImplicitAs(i32)] BigInt as AddTo(T) { ... }
 ```
 
-Wildcard impls must always be [external](#external-impl), to avoid having the
-names in the interface defined for the type multiple times.
+Wildcard impl declarations must always be [external](#external-impl), to avoid
+having the names in the interface defined for the type multiple times.
 
 ### Combinations
 
-The different kinds of parameters to impls may be combined. For example, if `T`
-implements `As(U)`, then this implements `As(Optional(U))` for `Optional(T)`:
+The different kinds of parameters to an `impl` declarations may be combined. For
+example, if `T` implements `As(U)`, then this implements `As(Optional(U))` for
+`Optional(T)`:
 
 ```
 external impl forall [U:! type, T:! As(U)]
@@ -3999,8 +3999,8 @@ impl Foo(?, i32) as Bar(String, ?)
 To get a uniform representation across different `impl` definitions, before type
 parameters are replaced the declarations are normalized as follows:
 
--   For impls declared lexically inline in a class definition, the type is added
-    between the `impl` and `as` keywords if the type is left out.
+-   For impl declarations lexically inline in a class definition, the type is
+    added between the `impl` and `as` keywords if the type is left out.
 -   Pointer types `T*` are replaced with `Ptr(T)`.
 -   The `external` keyword is removed, if present.
 -   The `forall` clause introducing type parameters is removed, if present.
@@ -4018,9 +4018,9 @@ library depends on.
 
 To achieve coherence, we need to ensure that any given impl can only be defined
 in a library that must be imported for it to apply. Specifically, given a
-specific type and specific interface, impls that can match can only be in
-libraries that must have been imported to name that type or interface. This is
-achieved with the _orphan rule_.
+specific type and specific interface, `impl` declarations that can match can
+only be in libraries that must have been imported to name that type or
+interface. This is achieved with the _orphan rule_.
 
 **Orphan rule:** Some name from the type structure of an `impl` declaration must
 be defined in the same library as the `impl`, that is some name must be _local_.
@@ -4031,17 +4031,18 @@ sufficient since it
 [need not be imported](/proposals/p0920.md#orphan-rule-could-consider-interface-requirements-in-blanket-impls).
 
 Since Carbon in addition requires there be no cyclic library dependencies, we
-conclude that there is at most one library that can define impls with a
-particular type structure.
+conclude that there is at most one library that can contain `impl` definitions
+with a particular type structure.
 
 #### Overlap rule
 
 Given a specific concrete type, say `Foo(bool, i32)`, and an interface, say
-`Bar(String, f32)`, the overlap rule picks, among all the matching impls, which
-type structure is considered "most specific" to use as the implementation of
-that type for that interface.
+`Bar(String, f32)`, the overlap rule picks, among all the matching `impl`
+declarations, which type structure is considered "most specific" to use as the
+implementation of that type for that interface.
 
-Given two different type structures of impls matching a query, for example:
+Given two different type structures of impl declarations matching a query, for
+example:
 
 ```
 impl Foo(?, i32) as Bar(String, ?)
@@ -4059,14 +4060,15 @@ difference.
 
 #### Prioritization rule
 
-Since at most one library can define impls with a given type structure, all
-impls with a given type structure must be in the same library. Furthermore by
-the [impl declaration access rules](#access), they will be defined in the API
-file for the library if they could match any query from outside the library. If
-there is more than one impl with that type structure, they must be
-[defined](#implementing-interfaces) or [declared](#declaring-implementations)
-together in a prioritization block. Once a type structure is selected for a
-query, the first impl in the prioritization block that matches is selected.
+Since at most one library can contain `impl` definitions with a given type
+structure, all `impl` definitions with a given type structure must be in the
+same library. Furthermore by the [impl declaration access rules](#access), they
+will be defined in the API file for the library if they could match any query
+from outside the library. If there is more than one impl with that type
+structure, they must be [defined](#implementing-interfaces) or
+[declared](#declaring-implementations) together in a prioritization block. Once
+a type structure is selected for a query, the first impl in the prioritization
+block that matches is selected.
 
 **Open question:** How are prioritization blocks written? A block starts with a
 keyword like `match_first` or `impl_priority` and then a sequence of impl
@@ -4084,12 +4086,13 @@ match_first {
 when they contain a mixture of type structures? There are three options:
 
 -   Prioritization blocks implicitly define all non-empty intersections of
-    contained impls, which are then selected by their type structure.
+    contained `impl` declarations, which are then selected by their type
+    structure.
 -   The compiler first picks the impl with the type pattern most favored for the
     query, and then picks the definition of the highest priority matching impl
     in the same prioritization block.
--   All the impls in a prioritization block are required to have the same type
-    structure, at a cost in expressivity.
+-   All the `impl` declarations in a prioritization block are required to have
+    the same type structure, at a cost in expressivity.
 
 To see the difference between the first two options, consider two libraries with
 type structures as follows:
@@ -4115,8 +4118,8 @@ interface) pairs where there is an edge from pair A to pair B if whether type A
 implements interface A determines whether type B implements interface B.
 
 The test for whether something forms a cycle needs to be precise enough, and not
-erase too much information when considering this graph, that these impls are not
-considered to form cycles with themselves:
+erase too much information when considering this graph, that these `impl`
+declarations are not considered to form cycles with themselves:
 
 ```
 impl forall [T:! Printable] Optional(T) as Printable;
@@ -4135,8 +4138,8 @@ This is a cycle where which types implement `ComparableWith` determines which
 types implement the same interface.
 
 **Example:** Cycles can create situations where there are multiple ways of
-selecting impls that are inconsistent with each other. Consider an interface
-with two blanket `impl` declarations:
+selecting `impl` declarations that are inconsistent with each other. Consider an
+interface with two blanket `impl` declarations:
 
 ```
 class Y {}
@@ -4145,18 +4148,18 @@ interface True {}
 impl Y as True {}
 interface Z(T:! type) { let Cond:! type; }
 match_first {
-  impl forall [T:! type, U:! Z(T) where .Cond is True] T as Z(U)
+  impl forall [T:! type, U:! Z(T) where .Cond impls True] T as Z(U)
       where .Cond = N { }
   impl forall [T:! type, U:! type] T as Z(U)
       where .Cond = Y { }
 }
 ```
 
-What is `i8.(Z(i16).Cond)`? It depends on which of the two blanket impls are
-selected.
+What is `i8.(Z(i16).Cond)`? It depends on which of the two blanket impl
+declarations are selected.
 
 -   An implementation of `Z(i16)` for `i8` could come from the first blanket
-    impl with `T == i8` and `U == i16` if `i16 is Z(i8)` and
+    impl with `T == i8` and `U == i16` if `i16 impls Z(i8)` and
     `i16.(Z(i8).Cond) == Y`. This condition is satisfied if `i16` implements
     `Z(i8)` using the second blanket impl. In this case,
     `i8.(Z(i16).Cond) == N`.
@@ -4209,8 +4212,8 @@ only detected by its users.
 **Open question:** Should Carbon reject cycles in the absence of a query? The
 two options here are:
 
--   Combining impls gives you an immediate error if there exists queries using
-    those impls that have cycles.
+-   Combining `impl` declarations gives you an immediate error if there exists
+    queries using them that have cycles.
 -   Only when a query reveals a cyclic dependency is an error reported.
 
 **Open question:** In the second case, should we ignore cycles if they don't
@@ -4219,20 +4222,21 @@ implementations that are lower priority.
 
 #### Termination rule
 
-It is possible to define a set of impls where there isn't a cycle, but the graph
-is infinite. Without some rule to prevent exhaustive exploration of the graph,
-determining whether a type implements an interface could run forever.
+It is possible to have a set of `impl` declarations where there isn't a cycle,
+but the graph is infinite. Without some rule to prevent exhaustive exploration
+of the graph, determining whether a type implements an interface could run
+forever.
 
-**Example:** It could be that `A` implements `B`, so `A is B` if
-`Optional(A) is B`, if `Optional(Optional(A)) is B`, and so on. This could be
-the result of a single impl:
+**Example:** It could be that `A` implements `B`, so `A impls B` if
+`Optional(A) impls B`, if `Optional(Optional(A)) impls B`, and so on. This could
+be the result of a single impl:
 
 ```
-impl forall [A:! type where Optional(.Self) is B] A as B { ... }
+impl forall [A:! type where Optional(.Self) impls B] A as B { ... }
 ```
 
-This problem can also result from a chain of impls, as in `A is B` if `A* is C`,
-if `Optional(A) is B`, and so on.
+This problem can also result from a chain of `impl` declarations, as in
+`A impls B` if `A* impls C`, if `Optional(A) impls B`, and so on.
 
 Rust solves this problem by imposing a recursion limit, much like C++ compilers
 use to terminate template recursion. This goes against
@@ -4250,7 +4254,7 @@ allow our desired use cases, but allow the compiler to detect non-terminating
 cases? Perhaps there is some sort of complexity measure Carbon can require
 doesn't increase when recursing?
 
-### `final` impls
+### `final` impl declarations
 
 There are cases where knowing that a parameterized impl won't be specialized is
 particularly valuable. This could let the compiler know the return type of a
@@ -4332,10 +4336,11 @@ fn F[T:! type](x: T) {
 }
 ```
 
-#### Libraries that can contain `final` impls
+#### Libraries that can contain a `final` impl
 
-To prevent the possibility of two unrelated libraries defining conflicting
-impls, Carbon restricts which libraries may declare an impl as `final` to only:
+To prevent the possibility of two unrelated libraries defining conflicting impl
+declarations, Carbon restricts which libraries may declare an impl as `final` to
+only:
 
 -   the library declaring the impl's interface and
 -   the library declaring the root of the `Self` type.
@@ -4352,19 +4357,19 @@ higher-priority impl is defined superseding a `final` impl.
 
 -   An impl with type structure `impl MyType(...) as MyInterface(...)` defined
     in the library with `MyType` must import the library defining `MyInterface`,
-    and so will be able to see any final blanket impls.
+    and so will be able to see any final blanket impl declarations.
 -   A blanket impl with type structure
     `impl ? as MyInterface(...ParameterType(...)...)` may be defined in the
     library with `ParameterType`, but that library must import the library
-    defining `MyInterface`, and so will be able to see any `final` blanket impls
-    that might overlap. A final impl with type structure
+    defining `MyInterface`, and so will be able to see any `final` blanket impl
+    declarations that might overlap. A final impl with type structure
     `impl MyType(...) as MyInterface(...)` would be given priority over any
     overlapping blanket impl defined in the `ParameterType` library.
 -   An impl with type structure
     `impl MyType(...ParameterType(...)...) as MyInterface(...)` may be defined
     in the library with `ParameterType`, but that library must import the
     libraries defining `MyType` and `MyInterface`, and so will be able to see
-    any `final` impls that might overlap.
+    any `final` `impl` declarations that might overlap.
 
 ### Comparison to Rust
 
@@ -4378,13 +4383,14 @@ differences between the Carbon and Rust plans:
 
 -   A Rust impl defaults to not being able to be specialized, with a `default`
     keyword used to opt-in to allowing specialization, reflecting the existing
-    code base developed without specialization. Carbon impls default to allowing
-    specialization, with restrictions on which may be declared `final`.
--   Since Rust impls are not specializable by default, generic functions can
-    assume that if a matching blanket impl is found, the associated types from
-    that impl will be used. In Carbon, if a generic function requires an
-    associated type to have a particular value, the function commonly will need
-    to state that using an explicit constraint.
+    code base developed without specialization. Carbon `impl` declarations
+    default to allowing specialization, with restrictions on which may be
+    declared `final`.
+-   Since a Rust impl is not specializable by default, generic functions can
+    assume that if a matching blanket impl declaration is found, the associated
+    types from that impl will be used. In Carbon, if a generic function requires
+    an associated type to have a particular value, the function commonly will
+    need to state that using an explicit constraint.
 -   Carbon will not have the "fundamental" attribute used by Rust on types or
     traits, as described in
     [Rust RFC 1023: "Rebalancing Coherence"](https://rust-lang.github.io/rfcs/1023-rebalancing-coherence.html).
@@ -4399,8 +4405,8 @@ differences between the Carbon and Rust plans:
     [Little Orphan Impls: The ordered rule](http://smallcultfollowing.com/babysteps/blog/2015/01/14/little-orphan-impls/#the-ordered-rule),
     but the specifics are different.
 -   Carbon is not planning to support any inheritance of implementation between
-    impls. This is more important to Rust since Rust does not support class
-    inheritance for implementation reuse. Rust has considered multiple
+    impl definitions. This is more important to Rust since Rust does not support
+    class inheritance for implementation reuse. Rust has considered multiple
     approaches here, see
     [Aaron Turon: "Specialize to Reuse"](http://aturon.github.io/tech/2015/09/18/reuse/)
     and
@@ -4481,9 +4487,9 @@ be used in the following contexts:
     `as C; }`
     -   Nothing implied by implementing `C` will be visible until `C` is
         complete.
--   ✅ `T:! C` ... `T is C`
--   ✅ `T:! A & C` ... `T is C`
-    -   This includes constructs requiring `T is C` such as `T as C` or
+-   ✅ `T:! C` ... `T impls C`
+-   ✅ `T:! A & C` ... `T impls C`
+    -   This includes constructs requiring `T impls C` such as `T as C` or
         `U:! C = T`.
 -   ✅ `external impl `...` as C;`
     -   Checking that all associated constants of `C` are correctly assigned
@@ -4496,7 +4502,7 @@ An incomplete `C` cannot be used in the following contexts:
 -   ❌ `class `...` { impl as C; }`
     -   The names of `C` are added to the class, and so those names need to be
         known.
--   ❌ `T:! C` ... `T is A` where `A` is an interface or named constraint
+-   ❌ `T:! C` ... `T impls A` where `A` is an interface or named constraint
     different from `C`
     -   Need to see the definition of `C` to see if it implies `A`.
 -   ❌ `external impl` ... `as C {` ... `}`
@@ -4540,9 +4546,9 @@ these rules:
 
 -   The definition must be in the same library as the declaration. They must
     either be in the same file, or the declaration can be in the API file and
-    the definition in an impl file. **Future work:** Carbon may require the
-    definition of [parameterized impls](#parameterized-impls) to be in the API
-    file, to support separate compilation.
+    the definition in an impl file. **Future work:** Carbon may require
+    [parameterized impl definitions](#parameterized-impl-declarations) to be in
+    the API file, to support separate compilation.
 -   If there is both a forward declaration and a definition, only the first
     declaration must specify the assignment of associated constants with a
     `where` clause. Later declarations may omit the `where` clause by writing
@@ -4684,11 +4690,13 @@ class MyClass {
 // from the API file to the implementation file for
 // this library.
 
-// Definition of previously declared external impls.
+// Definition of implementations previously declared
+// external.
 external impl MyClass as Interface2 where _ { }
 external impl MyClass as Interface5 where _ { }
 
-// Definition of previously declared internal impls.
+// Definition of implementations previously declared
+// internal.
 impl MyClass as Interface4 where _ { }
 impl MyClass as Interface6 where _ { }
 ```
@@ -4886,8 +4894,8 @@ interface TotalOrder {
 }
 ```
 
-The workaround for this restriction is to use a [blanket impl](#blanket-impls)
-instead:
+The workaround for this restriction is to use a
+[blanket impl declaration](#blanket-impl-declarations) instead:
 
 ```
 interface TotalOrder {
@@ -4916,7 +4924,7 @@ Rust has found them valuable.
 
 As an alternative to providing a definition of an interface member as a default,
 members marked with the `final` keyword will not allow that definition to be
-overridden in impls.
+overridden in `impl` definitions.
 
 ```
 interface TotalOrder {
@@ -5060,7 +5068,7 @@ fn ProcessVector(v: Vector(i32)) {
 }
 
 // Satisfies the requirement that `Vector(i32)` must
-// implement `Equatable` since `i32` is `Equatable`.
+// implement `Equatable` since `i32` impls `Equatable`.
 external impl forall [T:! Equatable] Vector(T) as Equatable { ... }
 ```
 
@@ -5080,7 +5088,7 @@ class Foo(T:! type) {}
 // This is allowed because we know that an `impl Foo(T) as Equatable`
 // will exist for all types `T` for which this impl is used, even
 // though there's neither an imported impl nor an impl in this file.
-external impl forall [T:! type where Foo(T) is Equatable]
+external impl forall [T:! type where Foo(T) impls Equatable]
     Foo(T) as Iterable {}
 ```
 
@@ -5090,7 +5098,7 @@ already satisfy the requirement of implementing `Iterable`:
 ```
 class Bar {}
 external impl Foo(Bar) as Equatable {}
-// Gives `Foo(Bar) is Iterable` using the blanket impl of
+// Gives `Foo(Bar) impls Iterable` using the blanket impl of
 // `Iterable` for `Foo(T)`.
 ```
 
@@ -5114,10 +5122,10 @@ visible implementation of `A` with the same `T` parameter for those types with
 the `.Result` associated type set to `i32`. That is
 [not sufficient](/proposals/p1088.md#less-strict-about-requirements-with-where-clauses),
 though, unless the implementation of `A` can't be specialized, either because it
-is [marked `final`](#final-impls) or is not
-[parameterized](#parameterized-impls). Implementations in other libraries can't
-make `A` be implemented for fewer types, but can cause `.Result` to have a
-different assignment.
+is [marked `final`](#final-impl-declarations) or is not
+[parameterized](#parameterized-impl-declarations). Implementations in other
+libraries can't make `A` be implemented for fewer types, but can cause `.Result`
+to have a different assignment.
 
 ## Observing a type implements an interface
 
@@ -5133,7 +5141,7 @@ One situation where this occurs is when there is a chain of
 [interfaces requiring other interfaces](#interface-requiring-other-interfaces-revisited).
 During the `impl` validation done during type checking, Carbon will only
 consider the interfaces that are direct requirements of the interfaces the type
-is known to implement. An `observe...is` declaration can be used to add an
+is known to implement. An `observe...impls` declaration can be used to add an
 interface that is a direct requirement to the set of interfaces whose direct
 requirements will be considered for that type. This allows a developer to
 provide a proof that there is a sequence of requirements that demonstrate that a
@@ -5154,32 +5162,33 @@ fn RequiresD[T:! D](x: T) {
   // ❌ Illegal: No direct connection between `D` and `A`.
   // RequiresA(x);
 
-  // `T` is `D` and `D` directly requires `C` to be
+  // `T` impls `D` and `D` directly requires `C` to be
   // implemented.
-  observe T is C;
+  observe T impls C;
 
-  // `T` is `C` and `C` directly requires `B` to be
+  // `T` impls `C` and `C` directly requires `B` to be
   // implemented.
-  observe T is B;
+  observe T impls B;
 
-  // ✅ Allowed: `T` is `B` and `B` directly requires
+  // ✅ Allowed: `T` impls `B` and `B` directly requires
   //             `A` to be implemented.
   RequiresA(x);
 }
 ```
 
-Note that `observe` statements do not affect the selection of impls during code
+Note that `observe` statements do not affect which impl is selected during code
 generation. For coherence, the impl used for a (type, interface) pair must
 always be the same, independent of context. The
 [termination rule](#termination-rule) governs when compilation may fail when the
 compiler can't determine the impl to select.
 
-### Observing blanket impls
+### Observing blanket impl declarations
 
-An `observe...is` declaration can also be used to observe that a type implements
-an interface because there is a [blanket impl](#blanket-impls) in terms of
-requirements a type is already known to satisfy. Without an `observe`
-declaration, Carbon will only use blanket impls that are directly satisfied.
+An `observe...impls` declaration can also be used to observe that a type
+implements an interface because there is a
+[blanket impl declaration](#blanket-impl-declarations) in terms of requirements
+a type is already known to satisfy. Without an `observe` declaration, Carbon
+will only use blanket impl declarations that are directly satisfied.
 
 ```
 interface A { }
@@ -5205,11 +5214,11 @@ fn RequiresA(T:! A)(x: T) {
 
   // There is a blanket implementation of `B` for
   // types implementing `A`.
-  observe T is B;
+  observe T impls B;
 
   // There is a blanket implementation of `C` for
   // types implementing `B`.
-  observe T is C;
+  observe T impls C;
 
   // ✅ Allowed: There is a blanket implementation
   //             of `D` for types implementing `C`.
@@ -5218,8 +5227,8 @@ fn RequiresA(T:! A)(x: T) {
 ```
 
 In the case of an error, a quality Carbon implementation will do a deeper search
-for chains of requirements and blanket impls and suggest `observe` declarations
-that would make the code compile if any solution is found.
+for chains of requirements and blanket impl declarations and suggest `observe`
+declarations that would make the code compile if any solution is found.
 
 ## Operator overloading
 
@@ -5401,7 +5410,7 @@ external impl forall [T:! ImplicitAs(f64)]
   }
 }
 // ✅ Allowed: uses `Meters as MultipliableWith(T)` impl
-//             with `T == f32` since `f32 is ImplicitAs(f64)`.
+//             with `T == f32` since `f32 impls ImplicitAs(f64)`.
 var now_allowed: Meters = height * scale;
 ```
 
@@ -5430,11 +5439,12 @@ equivalent to "implementation one". The second implementation replaces the
 `like f64` with a parameter that ranges over types that can be implicitly
 converted to `f64`, equivalent to "implementation two".
 
-In general, each `like` adds one additional impl. There is always the impl with
-all of the `like` expressions replaced by their arguments with the definition
-supplied in the source code. In addition, for each `like` expression, there is
-an impl with it replaced by a new parameter. These additional impls will
-delegate to the main impl, which will trigger implicit conversions according to
+In general, each `like` adds one additional parameterized implementation. There
+is always the impl defined with all of the `like` expressions replaced by their
+arguments with the definition supplied in the source code. In addition, for each
+`like` expression, there is an automatic `impl` definition with it replaced by a
+new parameter. These additional automatic implementations will delegate to the
+main impl, which will trigger implicit conversions according to
 [Carbon's ordinary implicit conversion rules](/docs/design/expressions/implicit_conversions.md).
 In this example, there are two uses of `like`, producing three implementations
 
@@ -5512,12 +5522,12 @@ external impl forall [T:! ImplicitAs(String)] Vector(T) as Printable;
 ```
 
 The generated implementations must be legal or the `like` is illegal. For
-example, it must be legal to define those impls in this library by the
-[orphan rule](#orphan-rule). In addition, the generated `impl` definitions must
-only require implicit conversions that are guaranteed to exist. For example,
-there existing an implicit conversion from `T` to `String` does not imply that
-there is one from `Vector(T)` to `Vector(String)`, so the following use of
-`like` is illegal:
+example, it must be legal to have those `impl` definitions in this library by
+the [orphan rule](#orphan-rule). In addition, the generated `impl` definitions
+must only require implicit conversions that are guaranteed to exist. For
+example, there existing an implicit conversion from `T` to `String` does not
+imply that there is one from `Vector(T)` to `Vector(String)`, so the following
+use of `like` is illegal:
 
 ```
 // ❌ Illegal: Can't convert a value with type
@@ -5648,7 +5658,7 @@ interface OptionalStorage {
 ```
 
 The default implementation of this interface is provided by a
-[blanket implementation](#blanket-impls):
+[blanket implementation](#blanket-impl-declarations):
 
 ```
 // Default blanket implementation
@@ -5776,7 +5786,7 @@ supported and made safe.
 The idea is that you would write tests alongside an interface that validate the
 expected behavior of any type implementing that interface.
 
-### Impls with state
+### Impl with state
 
 A feature we might consider where an `impl` itself can have state.
 
@@ -5850,3 +5860,4 @@ parameter, as opposed to an associated type, as in `N:! u32 where ___ >= 2`.
 -   [#2107: Clarify rules around `Self` and `.Self`](https://github.com/carbon-language/carbon-lang/pull/2107)
 -   [#2347: What can be done with an incomplete interface](https://github.com/carbon-language/carbon-lang/pull/2347)
 -   [#2376: Constraints must use `Self`](https://github.com/carbon-language/carbon-lang/pull/2376)
+-   [#2483: Replace keyword `is` with `impls`](https://github.com/carbon-language/carbon-lang/pull/2483)

docs/design/generics/overview.md

@@ -34,7 +34,7 @@ pointers to other design documents that dive deeper into individual topics.
         -   [Associated types](#associated-types)
         -   [Parameterized interfaces](#parameterized-interfaces)
     -   [Constraints](#constraints)
-    -   [Parameterized impls](#parameterized-impls)
+    -   [Parameterized impl declarations](#parameterized-impl-declarations)
     -   [Operator overloading](#operator-overloading)
 -   [Future work](#future-work)
 -   [References](#references)
@@ -594,7 +594,7 @@ fn FindFirstPrime[T:! Container where .Element == i32]
   ...
 }
 
-fn PrintContainer[T:! Container where .Element is Printable](c: T) {
+fn PrintContainer[T:! Container where .Element impls Printable](c: T) {
   // The type of the elements of `c` is not known, but we do know
   // that type satisfies the `Printable` interface.
   ...
@@ -614,7 +614,7 @@ class Vector(T:! Movable) {
 }
 ```
 
-### Parameterized impls
+### Parameterized impl declarations
 
 Implementations can be parameterized to apply to multiple types. Those
 parameters can have constraints to restrict when the implementation applies.

docs/design/generics/terminology.md

@@ -27,7 +27,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Nominal interfaces](#nominal-interfaces)
     -   [Named constraints](#named-constraints)
 -   [Associated entity](#associated-entity)
--   [Impls: Implementations of interfaces](#impls-implementations-of-interfaces)
+-   [Impl: Implementation of an interface](#impl-implementation-of-an-interface)
     -   [Internal impl](#internal-impl)
     -   [External impl](#external-impl)
 -   [Member access](#member-access)
@@ -308,7 +308,7 @@ form.
 
 A "nominal" interface is one where we say a type can only satisfy an interface
 if there is some explicit statement saying so, for example by defining an
-[impl](#impls-implementations-of-interfaces). This allows "satisfies the
+[impl](#impl-implementation-of-an-interface). This allows "satisfies the
 interface" to have additional semantic meaning beyond what is directly checkable
 by the compiler. For example, knowing whether the `Draw` function means "render
 an image to the screen" or "take a card from the top of a deck of cards"; or
@@ -338,18 +338,19 @@ type_.
 
 Different types can satisfy an interface with different definitions for a given
 member. These definitions are _associated_ with what type is implementing the
-interface. An [impl](#impls-implementations-of-interfaces) defines what is
+interface. An [impl](#impl-implementation-of-an-interface) defines what is
 associated with the type for that interface.
 
 Rust uses the term
 ["associated item"](https://doc.rust-lang.org/reference/items/associated-items.html)
 instead of associated entity.
 
-## Impls: Implementations of interfaces
+## Impl: Implementation of an interface
 
 An _impl_ is an implementation of an interface for a specific type. It is the
 place where the function bodies are defined, values for associated types, etc.
-are given. Impls are needed for [nominal interfaces](#nominal-interfaces);
+are given. Implementations are needed for
+[nominal interfaces](#nominal-interfaces);
 [structural interfaces](#structural-interfaces) and
 [named constraints](#named-constraints) define conformance implicitly instead of
 by requiring an impl to be defined. In can still make sense to implement a named
@@ -686,11 +687,12 @@ interface determines the type, not the caller. For example, the iterator type
 for a container is specific to the container and not something you would expect
 a user of the interface to specify.
 
-If you have an interface with type parameters, a type can have multiple impls
-for different combinations of type parameters. As a result, type parameters may
-not be deduced in a function call. However, if the interface parameters are
-specified, a type can only have a single implementation of the given interface.
-This unique implementation choice determines the values of associated types.
+If you have an interface with type parameters, a type can have multiple matching
+impl declarations for different combinations of type parameters. As a result,
+type parameters may not be deduced in a function call. However, if the interface
+parameters are specified, a type can only have a single implementation of the
+given interface. This unique implementation choice determines the values of
+associated types.
 
 For example, we might have an interface that says how to perform addition with
 another type:

docs/design/lexical_conventions/words.md

@@ -57,10 +57,10 @@ The following words are interpreted as keywords:
 -   `friend`
 -   `if`
 -   `impl`
+-   `impls`
 -   `import`
 -   `in`
 -   `interface`
--   `is`
 -   `let`
 -   `library`
 -   `like`

docs/project/principles/information_accumulation.md

@@ -76,9 +76,10 @@ especially important to the coherence of generics and templates.
 -   Classes are incomplete until the end of their definition. Unlike in C++, any
     attempt to observe a property of an incomplete class that is not known until
     the class is complete renders the program invalid.
--   When an `impl` needs to be resolved, only those `impl`s that have already
-    been declared are considered. However, if a later `impl` would change the
-    result of any earlier `impl` lookup, the program is invalid.
+-   When an `impl` needs to be resolved, only those `impl` declarations that
+    have that appear earlier are considered. However, if a later `impl`
+    declaration would change the result of any earlier `impl` lookup, the
+    program is invalid.
 
 ## Exceptions
 

proposals/p0920.md

@@ -64,7 +64,7 @@ feature that resolves multiple impls applying.
 ## Proposal
 
 This is a proposal to add
-[a "parameterized impls" section to the generics design details](/docs/design/generics/details.md#parameterized-impls).
+[a "parameterized impls" section to the generics design details](/docs/design/generics/details.md#parameterized-impl-declarations).
 
 ## Rationale based on Carbon's goals
 

proposals/p0983.md

@@ -66,7 +66,7 @@ impl.
 ## Details
 
 Details are in
-[the added `final` impl section to the generics details design document](/docs/design/generics/details.md#final-impls).
+[the added `final` impl section to the generics details design document](/docs/design/generics/details.md#final-impl-declarations).
 
 ## Rationale based on Carbon's goals
 

proposals/p1088.md

@@ -141,7 +141,7 @@ each other even when they work separately. These were significant enough
 downsides that we wanted to see if we could live with the restrictions that
 allowed local checking first. We don't know if developers will want to declare
 their parameterized implementations `final` in this situation anyway, even with
-[the limitations on `final`](/docs/design/generics/details.md#libraries-that-can-contain-final-impls).
+[the limitations on `final`](/docs/design/generics/details.md#libraries-that-can-contain-a-final-impl).
 
 This problem was discussed in
 [the #generics channel on Discord](https://discord.com/channels/655572317891461132/941071822756143115/941089885475962940).

proposals/p2483.md

@@ -0,0 +1,178 @@
+# Replace keyword `is` with `impls`
+
+<!--
+Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+Exceptions. See /LICENSE for license information.
+SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+-->
+
+[Pull request](https://github.com/carbon-language/carbon-lang/pull/2483)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Abstract](#abstract)
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Rationale](#rationale)
+-   [Alternatives considered](#alternatives-considered)
+    -   [`T as C`](#t-as-c)
+    -   [`T: C`](#t-c)
+
+<!-- tocstop -->
+
+## Abstract
+
+Use the keyword `impls` instead of `is` when writing a `where` constraint that a
+type variable needs to implement an interface or named constraint.
+
+What was previously (provisionally) written:
+
+```
+fn Sort[T:! Container where .ElementType is Ordered](x: T*);
+```
+
+will now be written:
+
+```
+fn Sort[T:! Container where .ElementType impls Ordered](x: T*);
+```
+
+## Problem
+
+The `is` keyword has been used as a placeholder in `where` constraints
+expressing that a type variable is required to implement an interface or named
+constraint. It has been an open question what word should be used in that
+position since its original adoption in
+[#818](https://github.com/carbon-language/carbon-lang/pull/818). Since then,
+reasons to use a different word in this position have been discovered:
+
+-   The word "is" is unspecific and could represent many different
+    relationships.
+-   This specific relationship is not symmetric.
+-   We potentially want to use `is` as a keyword for another purpose.
+-   The precedent for `is` came from Swift where `x is T` means "`x` has the
+    type `T`". With the changes to Carbon generic semantics, particularly
+    [#2360: Types are values of type `type`](https://github.com/carbon-language/carbon-lang/pull/2360),
+    that is increasingly a poor fit for what we mean by this condition.
+
+## Background
+
+The `is` keyword as a constraint operator was introduced in
+[#818: Constraints for generics (generics details 3)](https://github.com/carbon-language/carbon-lang/pull/818),
+along with the open question about how to spell it.
+
+The choice of `is` in that proposal followed
+[`is` being Swift's type check operator](https://docs.swift.org/swift-book/LanguageGuide/TypeCasting.html#ID340),
+where `x is T` is `true` if `x` has type `T`. Note that there are differences
+between the `is` operator in Swift and what we have used it for in Carbon. In
+Swift, it is used to test whether a value dynamically has a specific derived
+type, when you have a value of a base class type and are using inheritance. In
+Carbon:
+
+-   it is used on types instead of values;
+-   it is about conformance to an interface (the equivalent of Swift's
+    protocols), and not about inheritance; and
+-   it is resolved at compile time.
+
+## Proposal
+
+Use the keyword `impls` instead of `is` when writing a `where` constraint that
+at type variable needs to implement an interface or named constraint. The
+specific changes are included in
+[the same PR as this proposal](https://github.com/carbon-language/carbon-lang/pull/2483).
+
+## Rationale
+
+This proposal is working towards Carbon's
+[code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write)
+goal:
+
+-   Examples read naturally using "implements" in the place of the `impls`
+    keyword, commonly matching how a comment would describe the constraint.
+-   More clearly communicates the relationship between the two sides and that
+    the relationship is not symmetric.
+-   If a function has a `where T impls C` constraint that is not satisfied for
+    some calling type `T`, the fix is for the caller to add an `impl T as C`
+    definition.
+
+## Alternatives considered
+
+One concern with using `impls` is the potential for confusion with the plural of
+`impl`, meaning "implementations," rather than acting as the verb "implements."
+We hope to mitigate that concern by avoiding use of "impls" to mean anything
+other than `impls` in our documentation. For example, we would say "`impl`
+declarations" instead of "`impl`s".
+
+Alternatives were considered in
+[#2495: Keyword to use in place of `is` in `where`...`is` constraints](https://github.com/carbon-language/carbon-lang/issues/2495).
+A number of alternatives were considered:
+
+-   `T is C`
+-   `T isa C`
+-   `T impls C`
+-   `T implements C`
+-   `T ~ C`
+-   `T: C`
+-   `T as C`
+-   `T impl C`
+-   `T impl as C`
+-   `impl T as C`
+
+The reasons against `is` were outlined in the [problem](#problem) and
+[rationale](#rationale) sections. Reasons against other alternatives:
+
+-   `isa` seems (much) too rooted in inheritance.
+-   `implements` is long but otherwise fine. This is a specific place where
+    being verbose has worrisome negative impact.
+-   `~` is already being considered for something a bit more fitting --
+    bidirectional convertibility of our type "equality" constraints.
+-   `impl` seems a bit clunky, and surprising to see in this position when it
+    usually isn't.
+-   `impl as` seems even more clunky
+-   `impl T as C` also seems even more clunky, and would be confusing with the
+    rules around rewrite constraints (different here from the use of
+    `impl T as C` in a type).
+
+In general there were concerns that the alternatives were confusing and risk
+appearing to mean something other than what it does.
+
+### `T as C`
+
+The keyword `as` received more consideration:
+
+-   Already a thing, and names the _facet_ that is required to exist.
+-   Already used in a facet-like-but-not-facet context for
+    `impl T as C { ... }`.
+-   Short, easy to read, etc.
+
+It had some disadvantages, though:
+
+-   Doesn't connect readers as directly and effectively to the need for an
+    `impl` to satisfy the constraint.
+-   Doesn't read as nicely in context:
+    `T:! C where C.ElementType as AddWith(i32)`. This was a big consideration in
+    deciding against using `as`.
+-   Underlying the above disadvantage, it doesn't fit into the model of a
+    boolean expression that should be true. Instead, it is a cast that should be
+    _possible_ or _meaningful_, which is somewhat different from the rest of the
+    things in a `where` clause.
+    -   However, "rewrite" constraints don't quite fit this model either.
+    -   When using `==` constraints, they don't actually imply any boolean
+        expression that would return true. In fact, at least my understanding is
+        that the `T == U` constraint _could_ be written as a boolean expression
+        but it would return _false_ even when the constraint holds.
+
+### `T: C`
+
+`T: C` matches how Swift and Rust write this, and is similar to the way you'd
+write the same constraint in an ordinary declaration, `T:! I`. This syntactic
+similarity is also a liability due to the differences in semantics when used in
+a `where` clause: the `where` clause doesn't make the names from `I` available
+in `T`, and it doesn't propagate `where .A = B` rewrites from `I` to `T`.
+
+There's also some concern that the use of `:` would make parameter lists hard to
+read when they contain embedded `where` clauses, like
+`T:! Container where .ElementType: Printable, U:! OtherConstraint`.