<commit_before>/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME> and <NAME>
-/
constant IO : Type → Type
constant functorIO : functor IO
constant monadIO : monad IO

attribute [instance] functorIO monadIO

constant put_str : string → IO unit
constant put_nat : nat → IO unit
constant get_line : IO string<commit_msg>chore(library/system/IO): suppress unnecessary universe<commit_after>/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME> and <NAME>
-/
constant IO.{l} : Type.{l} → Type.{l}
constant functorIO : functor IO
constant monadIO : monad IO

attribute [instance] functorIO monadIO

constant put_str : string → IO unit
constant put_nat : nat → IO unit
constant get_line : IO string
{'fraction_non_alphanumeric': 0.08647450110864745, 'fraction_numerical': 0.013303769401330377, 'mean_word_length': 4.751592356687898, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, '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': '199854', 'n_tokens_mistral': 276, 'n_tokens_neox': 257, 'n_words': 118}