src/HOL/Codegenerator_Test/Basic_Setup.thy
author wenzelm
Wed, 25 Jun 2025 16:35:25 +0200
changeset 82768 8f866fd6fae1
parent 82516 88f101c3cfe2
permissions -rw-r--r--
merged

(* Author: Florian Haftmann, TU Muenchen *)

section \<open>Basic setup\<close>

theory Basic_Setup
imports
  Complex_Main
begin

text \<open>Drop technical stuff from \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>

ML \<open>
structure Codegenerator_Test =
struct

fun drop_partial_term_of thy =
  let
    val tycos = Sign.logical_types thy;
    val consts = map_filter (try (curry (Axclass.param_of_inst thy)
      \<^const_name>\<open>Quickcheck_Narrowing.partial_term_of\<close>)) tycos;
  in
    thy
    |> fold Code.declare_unimplemented_global consts
  end;

end;
\<close>

text \<open>Avoid popular infix.\<close>

code_reserved (SML) upto

end