diff -r 03d019ee7d02 -r 88f101c3cfe2 src/HOL/Codegenerator_Test/Candidates.thy --- a/src/HOL/Codegenerator_Test/Candidates.thy Tue Apr 15 19:40:42 2025 +0200 +++ b/src/HOL/Codegenerator_Test/Candidates.thy Tue Apr 15 23:04:44 2025 +0200 @@ -5,7 +5,7 @@ theory Candidates imports - Complex_Main + Basic_Setup "HOL-Library.Library" "HOL-Library.Sorting_Algorithms" "HOL-Library.Subseq_Order" @@ -19,16 +19,7 @@ "HOL-Examples.Gauss_Numbers" begin -text \Drop technical stuff from \<^theory>\HOL.Quickcheck_Narrowing\ which is tailored towards Haskell\ - -setup \ -fn thy => -let - val tycos = Sign.logical_types thy; - val consts = map_filter (try (curry (Axclass.param_of_inst thy) - \<^const_name>\Quickcheck_Narrowing.partial_term_of\)) tycos; -in fold Code.declare_unimplemented_global consts thy end -\ +setup \Codegenerator_Test.drop_partial_term_of\ text \Simple example for the predicate compiler.\ @@ -40,10 +31,6 @@ code_pred sublist . -text \Avoid popular infix.\ - -code_reserved (SML) upto - text \Explicit check in \OCaml\ for correct precedence of let expressions in list expressions\ definition funny_list :: "bool list"