Theory Basic_Setup

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Basic setup›

theory Basic_Setup
imports
  Complex_Main
begin

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

ML ‹
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>‹Quickcheck_Narrowing.partial_term_of›)) tycos;
  in
    thy
    |> fold Code.declare_unimplemented_global consts
  end;

end;
›

text ‹Avoid popular infix.›

code_reserved (SML) upto

end