<commit_before>type synonym FunDep       :-> Type
type synonym CollectedCCs :-> Type

data type arguments CoAxiom  (indices: br)
data type arguments Branches (indices: br)
data type arguments Bind     (indices: b)
data type arguments Expr     (indices: b)

# Compute the transitive value dependency graph for
# CallArity.callArityAnalProgram and only dump those converted functions.<commit_msg>[core-coq] Successfully convert the giant mutually-recursive monster type!<commit_after>type synonym FunDep       :-> Type
type synonym CollectedCCs :-> Type

data type arguments CoAxiom  (indices: br)
data type arguments Branches (indices: br)
data type arguments Bind     (indices: b)
data type arguments Expr     (indices: b)

redefine Inductive IdInfo           : Type := .
redefine Inductive DataConBoxer     : Type := .
redefine Inductive CoAxiomRule      : Type := .
redefine Inductive BuiltInSynFamily : Type := .

# Compute the transitive value dependency graph for
# CallArity.callArityAnalProgram and only dump those converted functions.
{'fraction_non_alphanumeric': 0.06813819577735125, 'fraction_numerical': 0.0, 'mean_word_length': 4.163366336633663, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 7, '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': '2086796', 'n_tokens_mistral': 295, 'n_tokens_neox': 288, 'n_words': 114}