equal
deleted
inserted
replaced
6 Order types and ordinal arithmetic. |
6 Order types and ordinal arithmetic. |
7 |
7 |
8 The order type of a well-ordering is the least ordinal isomorphic to it. |
8 The order type of a well-ordering is the least ordinal isomorphic to it. |
9 *) |
9 *) |
10 |
10 |
11 OrderType = OrderArith + Ordinal + |
11 OrderType = OrderArith + OrdQuant + |
12 consts |
12 consts |
13 ordermap :: [i,i]=>i |
13 ordermap :: [i,i]=>i |
14 ordertype :: [i,i]=>i |
14 ordertype :: [i,i]=>i |
15 |
15 |
16 Ord_alt :: i => o |
16 Ord_alt :: i => o |