Clarify what types can extend a trait (#1823)

* Clarify what types can extend a trait * Apply suggestions from code review Co-authored-by: Mikaël Mayer <[email protected]> Co-authored-by: Mikaël Mayer <[email protected]>
dafny-lang · Feb 15, 2022 · 49836a6 · 49836a6
1 parent aa18280
commit 49836a6
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md
@@ -2315,10 +2315,11 @@ TraitDecl =
 ````
 
 A _trait_ is an abstract superclass, similar to an "interface" or
-"mixin".[^fn-traits]
+"mixin". A trait can be _extended_ only by another trait or
+by a class (and in the latter case we say that the class _implements_
+the trait). More specifically, algebraic datatypes cannot extend traits.[^fn-traits]
 
-[^fn-traits]: Traits are new to Dafny and are likely to evolve for a
-while.
+[^fn-traits]: Traits are new to Dafny and are likely to evolve for a while.
 
 The declaration of a trait is much like that of a class:
 ```dafny