equal
deleted
inserted
replaced
27 Code_Cardinality.eq_set |
27 Code_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 nlists |
32 ]] |
33 ]] |
33 |
34 |
34 text \<open> |
35 text \<open> |
35 If code generation fails with a message like |
36 If code generation fails with a message like |
36 \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>, |
37 \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>, |