(* Author: Ondrej Kuncar, TU Muenchen *) section ‹Pervasive test of code generator› theory Generate_Efficient_Datastructures imports Candidates "HOL-Library.DAList_Multiset" "HOL-Library.RBT_Mapping" "HOL-Library.RBT_Set" begin text ‹ The following code equations have to be deleted because they use lists to implement sets in the code generetor. › declare [[code drop: "Inf :: _ Predicate.pred set ⇒ _" "Sup :: _ Predicate.pred set ⇒ _" pred_of_set Wellfounded.acc Code_Cardinality.card' Code_Cardinality.finite' Code_Cardinality.subset' Code_Cardinality.eq_set Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm "Gcd :: _ poly set ⇒ _" "Lcm :: _ poly set ⇒ _" nlists ]] text ‹ If code generation fails with a message like ‹"List.set" is not a constructor, on left hand side of equation: ...›, feel free to add an RBT implementation for the corresponding operation or delete that code equation (see above). › export_code _ checking SML OCaml? Haskell? Scala end