<commit_before>(*  Title:      Code_Test_GHC.thy
    Author:     <NAME>, ETH Zurich

Test case for test_code on GHC
*)

theory Code_Test_GHC imports Code_Test begin

definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id"

test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC

value [GHC] "14 + 7 * -12 :: integer"

end<commit_msg>drop workaround addressed by d0d3c30806b4<commit_after>(*  Title:      Code_Test_GHC.thy
    Author:     <NAME>, ETH Zurich

Test case for test_code on GHC
*)

theory Code_Test_GHC imports Code_Test begin

test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC

value [GHC] "14 + 7 * -12 :: integer"

end
{'fraction_non_alphanumeric': 0.11077844311377245, 'fraction_numerical': 0.05389221556886228, 'mean_word_length': 3.5821917808219177, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2969760', 'n_tokens_mistral': 271, 'n_tokens_neox': 242, 'n_words': 81}