Skip to content

Commit

Permalink
Document change on comparison predicates in order.v
Browse files Browse the repository at this point in the history
  • Loading branch information
pi8027 committed Mar 16, 2020
1 parent bdb23c1 commit 5f12298
Showing 1 changed file with 31 additions and 0 deletions.
31 changes: 31 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,37 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
1.10 in newer versions by using the `mc_1_10.Num` module instead of the
`Num` module. However, instances of the number structures may require
changes.
+ In the development process of this version of Mathematical Components, the
ordering of arguments of comparison predicates `lcomparableP`,
`(lcomparable_)ltgtP`, `(lcomparable_)leP`, and `(lcomparable_)ltP` in
`order.v` has been changed as follows. This is a potential source of
incompatibilities.
* before the change:
```
lcomparableP x y : incomparel x y
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
(y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
ltgtP x y : comparel x y
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
(y `&` x) (x `&` y) (y `|` x) (x `|` y).
leP x y :
lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
ltP x y :
ltl_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
```
* after the change:
```
lcomparableP x y : incomparel x y
(y `&` x) (x `&` y) (y `|` x) (x `|` y)
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).
ltgtP x y : comparel x y
(y `&` x) (x `&` y) (y `|` x) (x `|` y)
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
leP x y :
lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).
ltP x y :
ltl_xor_ge x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y).
```

- Extended comparison predicates `leqP`, `ltnP`, and `ltngtP` in ssrnat to
allow case analysis on `minn` and `maxn`.
Expand Down

0 comments on commit 5f12298

Please sign in to comment.