equal
deleted
inserted
replaced
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Type "int" is a linear order |
6 Type "int" is a linear order |
7 *) |
7 *) |
8 |
8 |
9 Int = IntDef + |
9 Int = IntDef + |
10 |
10 |
11 instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le) |
11 instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le) |
12 instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero) |
12 instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero) |
13 instance int :: linorder (zle_linear) |
13 instance int :: linorder (zle_linear) |
14 |
14 |
15 constdefs |
15 constdefs |
16 nat :: int => nat |
16 nat :: int => nat |
17 "nat(Z) == if neg Z then 0 else (@ m. Z = int m)" |
17 "nat(Z) == if neg Z then 0 else (THE m. Z = int m)" |
18 |
18 |
19 defs |
19 defs |
20 zabs_def "abs(i::int) == if i < 0 then -i else i" |
20 zabs_def "abs(i::int) == if i < 0 then -i else i" |
21 |
21 |
22 end |
22 end |