diff --git a/report/derived.verb b/report/derived.verb index 746d37c94510d1c567379a57f570c7a2031e4fef..0b39d8d5b3e10bbff28f3e27fe3a59dd5e742318 100644 --- a/report/derived.verb +++ b/report/derived.verb @@ -156,12 +156,10 @@ declaration counting as smaller than later ones. For example, for the Derived comparisons always traverse constructors from left to right. These examples illustrate this property: -\bprog -@ - (1,undefined) == (2,undefined) @"\Rightarrow"@ False - (undefined,1) == (undefined,2) @"\Rightarrow"@ @"\bot"@ -@ -\eprog +\begin{quote} +@(1,undefined) == (2,undefined) @"\Rightarrow"@ False@\\ +@(undefined,1) == (undefined,2) @"\Rightarrow"@ @"\bot" +\end{quote} All derived operations of class @Eq@ and @Ord@ are strict in both arguments. For example, "@False <= @\bot" is "\bot", even though @False@ is the first constructor of the @Bool@ type.