src/HOL/Codegenerator_Test/Basic_Setup.thy
author paulson <lp15@cam.ac.uk>
Sun, 03 Aug 2025 20:34:24 +0100
changeset 82913 7c870287f04f
parent 82516 88f101c3cfe2
permissions -rw-r--r--
New lemmas about improper integrals and other things

(* 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