equal
deleted
inserted
replaced
53 '"List.set" is not a constructor, on left hand side of equation: ...', |
53 '"List.set" is not a constructor, on left hand side of equation: ...', |
54 the code equation in question has to be either deleted (like many others in this file) |
54 the code equation in question has to be either deleted (like many others in this file) |
55 or implemented for RBT trees. |
55 or implemented for RBT trees. |
56 *) |
56 *) |
57 |
57 |
58 export_code _ checking SML OCaml? Haskell? |
58 export_code _ checking SML OCaml? Haskell? Scala |
59 |
|
60 (* Extra setup to make Scala happy *) |
|
61 (* If the compilation fails with an error "ambiguous implicit values", |
|
62 read \<section>7.1 in the Code Generation Manual *) |
|
63 |
|
64 lemma [code]: |
|
65 "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}" |
|
66 unfolding gfp_def by blast |
|
67 |
|
68 lemma [code]: |
|
69 "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}" |
|
70 unfolding lfp_def by blast |
|
71 |
|
72 export_code _ checking Scala? |
|
73 |
59 |
74 end |
60 end |