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