equal
deleted
inserted
replaced
143 The constant \cdx{0} is also overloaded. It serves as the zero element of |
143 The constant \cdx{0} is also overloaded. It serves as the zero element of |
144 several types, of which the most important is \tdx{nat} (the natural |
144 several types, of which the most important is \tdx{nat} (the natural |
145 numbers). The type class \cldx{plus_ac0} comprises all types for which 0 |
145 numbers). The type class \cldx{plus_ac0} comprises all types for which 0 |
146 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These |
146 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These |
147 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also |
147 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also |
148 multisets. The summation operator \cdx{setsum} is available for all types in |
148 multisets. The summation operator \cdx{sum} is available for all types in |
149 this class. |
149 this class. |
150 |
150 |
151 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order |
151 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order |
152 signatures. The relations $<$ and $\leq$ are polymorphic over this |
152 signatures. The relations $<$ and $\leq$ are polymorphic over this |
153 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and |
153 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and |