equal
deleted
inserted
replaced
35 term "[1::int] = func" |
35 term "[1::int] = func" |
36 *) |
36 *) |
37 |
37 |
38 (* Coercion/type maps definitions *) |
38 (* Coercion/type maps definitions *) |
39 |
39 |
40 primrec nat_of_bool :: "bool \<Rightarrow> nat" |
40 abbreviation nat_of_bool :: "bool \<Rightarrow> nat" |
41 where |
41 where |
42 "nat_of_bool False = 0" |
42 "nat_of_bool \<equiv> of_bool" |
43 | "nat_of_bool True = 1" |
|
44 |
43 |
45 declare [[coercion nat_of_bool]] |
44 declare [[coercion nat_of_bool]] |
46 |
45 |
47 declare [[coercion int]] |
46 declare [[coercion int]] |
48 |
47 |
199 consts n :: nat m :: nat |
198 consts n :: nat m :: nat |
200 term "- (n + m)" |
199 term "- (n + m)" |
201 declare [[coercion_args uminus -]] |
200 declare [[coercion_args uminus -]] |
202 declare [[coercion_args plus + +]] |
201 declare [[coercion_args plus + +]] |
203 term "- (n + m)" |
202 term "- (n + m)" |
204 |
203 |
205 end |
204 end |