equal
deleted
inserted
replaced
165 This approach however fails if the representation of a type demands |
165 This approach however fails if the representation of a type demands |
166 invariants; this issue is discussed in the next section. |
166 invariants; this issue is discussed in the next section. |
167 *} |
167 *} |
168 |
168 |
169 |
169 |
170 subsection {* Datatype refinement involving invariants *} |
170 subsection {* Datatype refinement involving invariants \label{sec:invariant} *} |
171 |
171 |
172 text {* |
172 text {* |
173 Datatype representation involving invariants require a dedicated |
173 Datatype representation involving invariants require a dedicated |
174 setup for the type and its primitive operations. As a running |
174 setup for the type and its primitive operations. As a running |
175 example, we implement a type @{text "'a dlist"} of list consisting |
175 example, we implement a type @{text "'a dlist"} of list consisting |