From 49836a61395b18644193a6c48bde074d6652ba4e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 15 Feb 2022 14:28:41 -0800 Subject: [PATCH] Clarify what types can extend a trait (#1823) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Clarify what types can extend a trait * Apply suggestions from code review Co-authored-by: Mikaël Mayer Co-authored-by: Mikaël Mayer --- docs/DafnyRef/Types.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index daa8e322185..6e55c4ada8e 100644 --- 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