equal
deleted
inserted
replaced
29 definition max_nat :: "nat => nat => nat" |
29 definition max_nat :: "nat => nat => nat" |
30 where "max_nat a b = (if a <= b then b else a)" |
30 where "max_nat a b = (if a <= b then b else a)" |
31 |
31 |
32 lemma [code_pred_inline]: |
32 lemma [code_pred_inline]: |
33 "max = max_nat" |
33 "max = max_nat" |
34 by (simp add: ext_iff max_def max_nat_def) |
34 by (simp add: fun_eq_iff max_def max_nat_def) |
35 |
35 |
36 definition |
36 definition |
37 "max_of_my_Suc x = max x (Suc x)" |
37 "max_of_my_Suc x = max x (Suc x)" |
38 |
38 |
39 text {* In this example, max is specialised, hence the mode o => i => bool is possible *} |
39 text {* In this example, max is specialised, hence the mode o => i => bool is possible *} |