source:
src/utilities/adt/ordering.ma
| Last change on this file was 1208, checked in by , 9 years ago | |
|---|---|
| File size: 214 bytes | |
| Rev | Line | |
|---|---|---|
| [1208] | 1 | include "basics/types.ma". |
| 2 | ||
| 3 | inductive order: Type[0] ≝ | |
| 4 | | order_lt: order | |
| 5 | | order_gt: order | |
| 6 | | order_eq: order. | |
| 7 | ||
| 8 | record ordered (elt_type: Type[0]): Type[1] ≝ | |
| 9 | { | |
| 10 | order: elt_type → elt_type → order | |
| 11 | }. | |
| 12 |
Note: See TracBrowser
for help on using the repository browser.
