equal
deleted
inserted
replaced
27 Cardinality.eq_set |
27 Cardinality.eq_set |
28 Euclidean_Algorithm.Gcd |
28 Euclidean_Algorithm.Gcd |
29 Euclidean_Algorithm.Lcm |
29 Euclidean_Algorithm.Lcm |
30 "Gcd :: _ poly set \<Rightarrow> _" |
30 "Gcd :: _ poly set \<Rightarrow> _" |
31 "Lcm :: _ poly set \<Rightarrow> _" |
31 "Lcm :: _ poly set \<Rightarrow> _" |
32 permutations_of_set |
|
33 permutations_of_multiset |
|
34 ]] |
32 ]] |
35 |
33 |
36 text \<open> |
34 text \<open> |
37 If code generation fails with a message like |
35 If code generation fails with a message like |
38 \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>, |
36 \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>, |
39 feel free to add an RBT implementation for the corrsponding operation |
37 feel free to add an RBT implementation for the corresponding operation |
40 of delete that code equation (see above). |
38 or delete that code equation (see above). |
41 \<close> |
39 \<close> |
42 |
40 |
43 export_code _ checking SML OCaml? Haskell? Scala |
41 export_code _ checking SML OCaml? Haskell? Scala |
44 |
42 |
45 end |
43 end |