<commit_before>theory Code_haskell
imports
  "../Routing/IpRoute_Parser" (*TODO: sqrl strings don't get nicely exported to code! *)
  "../Primitive_Matchers/Parser"
begin

definition word_less_eq :: "('a::len) word \<Rightarrow> ('a::len) word \<Rightarrow> bool" where
  "word_less_eq a b \<equiv> a \<le> b"

definition word_to_nat :: "('a::len) word \<Rightarrow> nat" where
  "word_to_nat = Word.unat"


definition mk_Set :: "'a list \<Rightarrow> 'a set" where
  "mk_Set = set"

<commit_msg>fixed import<commit_after>theory Code_haskell
imports
  "../../Routing/IpRoute_Parser" (*TODO: sqrl strings don't get nicely exported to code! *)
  "../Primitive_Matchers/Parser"
begin

definition word_less_eq :: "('a::len) word \<Rightarrow> ('a::len) word \<Rightarrow> bool" where
  "word_less_eq a b \<equiv> a \<le> b"

definition word_to_nat :: "('a::len) word \<Rightarrow> nat" where
  "word_to_nat = Word.unat"


definition mk_Set :: "'a list \<Rightarrow> 'a set" where
  "mk_Set = set"


{'fraction_non_alphanumeric': 0.15995975855130784, 'fraction_numerical': 0.0, 'mean_word_length': 4.558659217877095, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 15, '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': '247665', 'n_tokens_mistral': 370, 'n_tokens_neox': 346, 'n_words': 103}