diff options
| author | letouzey | 2008-12-17 15:31:54 +0000 |
|---|---|---|
| committer | letouzey | 2008-12-17 15:31:54 +0000 |
| commit | 211030a7a870bdf3bc36b0923379e2d1bf6c729a (patch) | |
| tree | 9953a1d775fe3161d43ca32e7073d10ae10349e1 /CHANGES | |
| parent | 275151328893782671c1c6949c93b65f6d65fefa (diff) | |
FSet/OrderedType now includes an eq_dec, and hence become an extension of DecidableType
After lots of hesitations, OrderedType now requires this "eq_dec" field, which
is redundant (can be deduced from "compare"), but allows the subtyping relation
DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly
extensions of weak sets. Of course this change introduces a last-minute
incompatibility, but:
- There is a clear gain in term of functionnality / simplicity.
- FSets 8.2 already needs some adaptations when compared with 8.1, so it's
the right time to push such incompatible changes.
- Transition shouldn't be too hard: the old OrderedType still exists under
the name MiniOrderedType, and functor MOT_to_OT allows to convert from
one to the other.
Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType
(resp. OrderedType), an eq_dec on sets is now required in these interfaces
and in the implementations. In pratice, it is really easy to build from
equal and equal_1 and equal_2.
Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun,
while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M).
Idem with WDecide, WProperties and WEqProperties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -116,6 +116,11 @@ Libraries (DOC TO CHECK) thanks to new features of Coq modules (in particular Include), see FSetInterface. Same for maps. Hints in these interfaces have been reworked (they are now placed in a "set" database). + * To allow full subtyping between weak and ordered sets, a field + "eq_dec" has been added to OrderedType. The old version of OrderedType + is now called MiniOrderedType and functor MOT_to_OT allow to + convert to the new version. The interfaces and implementations + of sets now contain also such a "eq_dec" field. * FSetDecide, contributed by Aaron Bohannon, contains a decision procedure allowing to solve basic set-related goals (for instance, is a point in a particular set ?). See FSetProperties for examples. |