15 The following code equations have to be deleted because they use |
15 The following code equations have to be deleted because they use |
16 lists to implement sets in the code generetor. |
16 lists to implement sets in the code generetor. |
17 \<close> |
17 \<close> |
18 |
18 |
19 declare [[code drop: |
19 declare [[code drop: |
20 Sup_pred_inst.Sup_pred |
20 "Inf :: _ Predicate.pred set \<Rightarrow> _" |
21 Inf_pred_inst.Inf_pred |
21 "Sup :: _ Predicate.pred set \<Rightarrow> _" |
22 pred_of_set |
22 pred_of_set |
23 Wellfounded.acc |
23 Wellfounded.acc |
24 Cardinality.card' |
24 Cardinality.card' |
25 Cardinality.finite' |
25 Cardinality.finite' |
26 Cardinality.subset' |
26 Cardinality.subset' |
27 Cardinality.eq_set |
27 Cardinality.eq_set |
28 Gcd_fin |
28 Gcd_fin |
29 Lcm_fin |
29 Lcm_fin |
|
30 Euclidean_Algorithm.Gcd |
|
31 Euclidean_Algorithm.Lcm |
30 "Gcd :: nat set \<Rightarrow> nat" |
32 "Gcd :: nat set \<Rightarrow> nat" |
31 "Lcm :: nat set \<Rightarrow> nat" |
33 "Lcm :: nat set \<Rightarrow> nat" |
32 "Gcd :: int set \<Rightarrow> int" |
34 "Gcd :: int set \<Rightarrow> int" |
33 "Lcm :: int set \<Rightarrow> int" |
35 "Lcm :: int set \<Rightarrow> int" |
34 "Gcd :: _ poly set \<Rightarrow> _" |
36 "Gcd :: _ poly set \<Rightarrow> _" |
35 "Lcm :: _ poly set \<Rightarrow> _" |
37 "Lcm :: _ poly set \<Rightarrow> _" |
36 Euclidean_Algorithm.Gcd |
|
37 Euclidean_Algorithm.Lcm |
|
38 permutations_of_set |
38 permutations_of_set |
39 permutations_of_multiset |
39 permutations_of_multiset |
40 ]] |
40 ]] |
41 |
41 |
42 (* |
42 text \<open> |
43 If the code generation ends with an exception with the following message: |
43 If code generation fails with a message like |
44 '"List.set" is not a constructor, on left hand side of equation: ...', |
44 @{text \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>}, |
45 the code equation in question has to be either deleted (like many others in this file) |
45 feel free to add an RBT implementation for the corrsponding operation |
46 or implemented for RBT trees. |
46 of delete that code equation (see above). |
47 *) |
47 \<close> |
48 |
48 |
49 export_code _ checking SML OCaml? Haskell? Scala |
49 export_code _ checking SML OCaml? Haskell? Scala |
50 |
50 |
51 end |
51 end |