equal
deleted
inserted
replaced
74 "Lcm_eucl = Lcm_eucl" .. |
74 "Lcm_eucl = Lcm_eucl" .. |
75 |
75 |
76 lemma [code, code del]: |
76 lemma [code, code del]: |
77 "permutations_of_set = permutations_of_set" .. |
77 "permutations_of_set = permutations_of_set" .. |
78 |
78 |
|
79 lemma [code, code del]: |
|
80 "permutations_of_multiset = permutations_of_multiset" .. |
|
81 |
79 (* |
82 (* |
80 If the code generation ends with an exception with the following message: |
83 If the code generation ends with an exception with the following message: |
81 '"List.set" is not a constructor, on left hand side of equation: ...', |
84 '"List.set" is not a constructor, on left hand side of equation: ...', |
82 the code equation in question has to be either deleted (like many others in this file) |
85 the code equation in question has to be either deleted (like many others in this file) |
83 or implemented for RBT trees. |
86 or implemented for RBT trees. |