Update classifier db

1 files changed, 1830 insertions, 133 deletions

diff --git a/lib/linguist/classifier.yml b/lib/linguist/classifier.yml
index a3f051c..2e314ee 100644
--- a/lib/linguist/classifier.yml
+++ b/lib/linguist/classifier.yml
@@ -1,6 +1,6 @@
 --- !ruby/object:Linguist::Classifier
-languages_total: 218
-tokens_total: 152762
+languages_total: 241
+tokens_total: 172817
 languages:
   "Apex": 6
   "AppleScript": 2
@@ -10,7 +10,7 @@ languages:
   "C++": 14
   "Ceylon": 1
   "CoffeeScript": 9
-  "Coq": 1
+  "Coq": 12
   "Dart": 1
   "Delphi": 1
   "Diff": 1
@@ -61,7 +61,7 @@ languages:
   "Tea": 1
   "Turing": 1
   "VHDL": 1
-  "Verilog": 1
+  "Verilog": 13
   "VimL": 2
   "Visual Basic": 1
   "XML": 1
@@ -77,7 +77,7 @@ language_tokens:
   "C++": 8284
   "Ceylon": 50
   "CoffeeScript": 2340
-  "Coq": 1524
+  "Coq": 18324
   "Dart": 68
   "Delphi": 30
   "Diff": 16
@@ -128,7 +128,7 @@ language_tokens:
   "Tea": 3
   "Turing": 52
   "VHDL": 42
-  "Verilog": 190
+  "Verilog": 3445
   "VimL": 20
   "Visual Basic": 294
   "XML": 5505
@@ -5127,111 +5127,691 @@ tokens:
     "||": 3
     "}": 31
   "Coq":
-    "%": 1
-    "(": 130
-    ")": 132
-    "*": 38
-    "**": 11
-    "+": 3
-    "-": 13
-    ".": 57
-    "/": 1
-    "0": 1
-    ";": 33
-    "<": 38
-    "<->": 1
-    "<=>": 6
+    "%": 3
+    "&": 19
+    "(": 1293
+    ")": 1297
+    "*": 170
+    "**": 36
+    "**************************************************************": 1
+    "************************************************************************": 5
+    "*.": 58
+    "*Reserved": 1
+    "+": 227
+    "-": 456
+    ".": 463
+    ".*": 1
+    "..": 2
+    ".1": 1
+    "/": 36
+    "//": 1
+    "0": 5
+    "1": 6
+    "1999": 3
+    "2": 5
+    "2003": 1
+    "2006": 1
+    "2010": 3
+    "9": 1
+    "95": 1
+    ";": 378
+    "<": 79
+    "<----->": 2
+    "<---->": 1
+    "<->": 32
+    "<=>": 11
     "<=m}>": 3
     "<=n),>": 1
     "<=n}>": 1
     "<=n}|>": 1
-    "A": 19
+    "<O___,,>": 3
+    "@HdRel_inv": 2
+    "@In": 1
+    "@Permutation": 6
+    "@app": 1
+    "@if_eqA_rewrite_l": 2
+    "@length": 1
+    "@meq": 4
+    "@munion": 1
+    "@rev": 1
+    "A": 115
+    "A.": 3
+    "A1": 3
+    "A1.": 1
+    "A2": 4
+    "AExp.": 1
+    "AId": 19
+    "AMinus": 11
+    "AMult": 11
+    "ANum": 36
+    "APlus": 15
+    "Abs": 2
+    "Actually": 1
+    "Adapted": 1
+    "Alternative": 1
+    "Arguments": 13
     "Arith.": 2
+    "Assistant": 4
+    "B": 8
+    "BAnd": 5
+    "BD.": 1
+    "BEq": 6
+    "BFalse": 4
+    "BLe": 6
+    "BNot": 7
+    "BO": 4
+    "BTrue": 6
+    "Basics.": 2
+    "Bene": 1
+    "Building": 2
+    "CAss": 2
+    "CIf": 2
+    "CNRS": 4
+    "CSeq": 2
+    "CSkip": 1
+    "CSkip.": 1
+    "CWhile": 2
+    "Case": 48
+    "Case.": 1
+    "Case_aux": 45
+    "Coiso1.": 2
+    "Coiso2.": 3
+    "Compare_dec": 1
+    "ConT3": 1
     "Conclusion": 1
-    "Definition": 2
+    "Constructors": 2
+    "Context.": 1
+    "Copyright": 4
+    "Coq": 8
+    "D": 9
+    "DO": 5
+    "Defined.": 1
+    "Definition": 60
+    "Development": 4
+    "E": 9
+    "E.": 2
+    "E1": 2
+    "E1.": 1
+    "E2": 1
+    "E2.": 3
+    "ELSE": 3
+    "END": 2
+    "END.": 3
+    "EQ": 8
+    "EQ.": 2
+    "E_Ass": 2
+    "E_Ass.": 3
+    "E_Const": 2
+    "E_IfFalse.": 2
+    "E_Plus": 2
+    "E_Seq": 3
+    "E_Skip.": 1
+    "E_WhileEnd.": 1
+    "E_WhileLoop": 1
+    "EmptyBag": 2
+    "End": 13
     "Eqdep_dec.": 1
+    "Equivalence": 2
+    "Equivalence_Reflexive": 1
+    "Equivalence_Reflexive.": 1
+    "Example": 40
+    "Export": 10
+    "FI": 3
+    "Fact": 3
     "False.": 1
-    "H": 3
-    "H.": 2
+    "File": 1
+    "Fixpoint": 36
+    "For": 2
+    "Forall2": 1
+    "From": 3
+    "G": 7
+    "GNU": 4
+    "Gamma": 10
+    "General": 4
+    "Global": 4
+    "H": 77
+    "H.": 77
+    "H0": 15
+    "H0.": 9
+    "H1": 18
+    "H1.": 30
+    "H11": 2
+    "H11.": 1
+    "H12": 5
+    "H12.": 1
+    "H2": 14
+    "H2.": 18
+    "H21": 3
+    "H22": 2
+    "H22.": 1
+    "H3": 4
+    "H3.": 4
+    "H4": 5
+    "H4.": 1
+    "H6": 3
+    "HE": 1
+    "HE.": 1
     "HSnx": 1
     "HSnx.": 1
+    "HT": 1
+    "HT.": 1
+    "HT1.": 1
+    "HX": 1
+    "Ha": 6
+    "Ha.": 1
+    "Hafi.": 2
+    "Hal": 2
+    "Hce": 1
+    "Hce.": 1
+    "Hceval.": 2
+    "HdRel": 4
     "Hdec": 3
-    "Heq": 7
+    "He1": 2
+    "He1.": 1
+    "He2": 1
+    "He2.": 2
+    "Heap": 1
+    "HeapT3": 1
+    "Heq": 8
     "Heq.": 6
+    "HeqA.": 1
+    "HeqA1": 1
+    "HeqA1.": 1
+    "HeqCoiso1.": 1
+    "HeqCoiso2.": 1
     "HeqS": 3
     "HeqS.": 2
+    "Heqe.": 3
     "Heqf": 1
     "Heqf.": 2
     "Heqg": 1
+    "Heqm": 5
+    "Heqm.": 1
+    "Heqr": 3
+    "Heqr1": 1
+    "Heqst1": 4
     "Heqx": 4
     "Heqx.": 2
     "Heqy": 1
+    "Heval.": 4
+    "Hf": 15
+    "Hf.": 1
+    "Hf1": 1
+    "Hf2": 1
+    "Hf3": 2
     "Hfbound": 1
     "Hfbound.": 2
     "Hfinj": 1
     "Hfinj.": 3
     "Hfsurj": 2
     "Hfx": 2
+    "Hg": 2
     "Hgefx": 1
     "Hgefy": 1
     "Hginj": 1
     "Hgsurj": 3
     "Hgsurj.": 1
-    "Hle": 1
-    "Hle.": 1
+    "Hint": 8
+    "Hl": 3
+    "Hl.": 1
+    "Hle": 2
+    "Hle.": 2
     "Hlefx": 1
     "Hlefy": 1
     "Hlep": 4
     "Hlep.": 3
     "Hlt": 3
     "Hlt.": 1
+    "Hm": 1
     "Hmn": 1
     "Hmn.": 1
+    "Hmo": 1
+    "Hmo.": 4
+    "Hn": 1
     "Hneq": 7
     "Hneq.": 2
     "Hneqx": 1
     "Hneqx.": 2
     "Hneqy": 1
     "Hneqy.": 2
-    "Hp": 4
+    "Hnil": 1
+    "Hnm": 3
+    "Hnm.": 3
+    "Hp": 5
+    "Hperm": 4
+    "Hpermmm": 1
     "Hpq.": 1
     "Hq": 3
-    "Hx": 12
+    "Hskip": 3
+    "Hswap": 2
+    "Ht": 1
+    "Ht.": 3
+    "Htrans": 1
+    "Htrans.": 1
+    "Huet": 1
+    "Huffmann": 1
+    "Hx": 24
     "Hx.": 4
-    "Hy": 2
-    "Hy.": 2
+    "Hxx": 1
+    "Hy": 17
+    "Hy.": 3
     "Hy0": 1
+    "Hy1": 2
+    "Hy1.": 5
+    "Hy2": 3
+    "Hy2.": 2
+    "Hypothesis": 7
+    "IFB": 3
+    "IH": 4
+    "IHHT1.": 1
+    "IHHT2.": 1
+    "IHHce1": 1
+    "IHHce2": 1
+    "IHHmo.": 1
+    "IHHy1": 2
+    "IHP": 1
+    "IHP2": 1
+    "IHPermutation1": 1
+    "IHPermutation2": 1
+    "IHb": 1
+    "IHclos_refl_trans1.": 2
+    "IHclos_refl_trans2.": 2
+    "IHe1.": 11
+    "IHe2.": 10
+    "IHhas_type.": 1
+    "IHhas_type1.": 1
+    "IHhas_type2.": 1
+    "IHi": 3
+    "IHl": 8
+    "IHl.": 8
+    "IHl1": 1
+    "IHl1.": 1
+    "IHle.": 1
+    "IHm": 2
+    "IHm.": 1
+    "IHn": 13
+    "IHn.": 3
     "IHp": 2
-    "Import": 3
+    "IHp.": 2
+    "IHrefl_step_closure": 1
+    "IHrefl_step_closure.": 1
+    "IHs.": 2
+    "IHt.": 1
+    "IHt1": 2
+    "IHt1.": 1
+    "IHt2": 3
+    "IHt3": 1
+    "INRIA": 4
+    "Id": 8
+    "Immediate": 1
+    "Imp.": 1
+    "Implicit": 15
+    "Import": 11
+    "In": 8
+    "InA": 9
+    "InA_split": 2
+    "Indeed": 1
+    "Inductive": 38
+    "Injection": 1
+    "Instance": 6
+    "Inutilisable": 1
+    "Inversion": 2
+    "It": 1
+    "Jean": 1
     "K": 1
     "K_dec_set": 1
-    "Lemma": 3
+    "L12": 2
+    "LE": 11
+    "LE.": 3
+    "LIX": 4
+    "LRI": 4
+    "LT": 14
+    "LT.": 5
+    "Laurent": 1
+    "LeA": 1
+    "LeA.": 1
+    "Leaf": 1
+    "Leibniz": 1
+    "Lemma": 56
+    "Lesser": 4
+    "Let": 9
+    "License": 4
+    "List": 4
+    "ListNotations": 1
+    "Lists.": 1
+    "Local": 6
+    "Logic.": 1
+    "Logic.eq": 2
+    "Lt.S_pred": 3
+    "Lt.le_lt_or_eq": 3
+    "Lt.le_or_lt": 1
+    "Lt.lt_irrefl": 2
+    "Lt.lt_le_trans": 2
+    "Lt.lt_not_le": 2
+    "Ltac": 1
+    "M": 4
+    "Marc": 1
+    "May": 1
+    "Mergesort": 1
+    "Mergesort.": 1
+    "Merging": 1
+    "Minus.minus_Sn_m": 1
+    "Module": 9
+    "Morphisms": 1
+    "Morphisms.": 1
+    "Multiset": 3
+    "N": 2
+    "NEQ": 1
+    "NEW": 2
+    "NatList.": 2
+    "NoDup": 2
+    "NoDupA": 4
+    "NoDupA_equivlistA_permut": 1
+    "NoDup_Permutation": 1
+    "NoDup_Permutation_bis": 2
+    "NoDup_cardinal_incl": 2
+    "NoDup_remove_1": 1
+    "Node": 1
+    "None": 17
+    "None.": 2
+    "Nonsense.": 4
+    "Nota": 1
+    "Notation": 44
+    "Notin": 1
+    "O": 99
+    "O.": 4
+    "O___": 1
+    "October": 1
+    "Omega": 1
+    "P": 31
+    "P.": 5
+    "P1": 2
+    "P11": 1
+    "P11.": 1
+    "P12": 1
+    "P12.": 2
+    "P2": 1
+    "P2.": 1
+    "P21": 1
+    "P21.": 2
+    "P22": 1
+    "PD": 2
+    "PG": 2
+    "PL": 1
+    "PN.": 2
+    "PPS": 4
+    "Parameter": 1
+    "Permut": 1
+    "PermutSetoid": 1
+    "Permut_permut.": 1
+    "Permutation": 51
+    "Permutation_NoDup": 1
+    "Permutation_add_inside": 1
+    "Permutation_alt": 1
+    "Permutation_alt.": 1
+    "Permutation_app": 1
+    "Permutation_app.": 1
+    "Permutation_app_comm": 3
+    "Permutation_app_head": 1
+    "Permutation_app_inv": 2
+    "Permutation_app_inv_l": 1
+    "Permutation_app_inv_r": 1
+    "Permutation_app_swap": 1
+    "Permutation_app_tail": 1
+    "Permutation_cons_app": 2
+    "Permutation_cons_app_inv": 1
+    "Permutation_cons_append": 1
+    "Permutation_cons_append.": 3
+    "Permutation_cons_inv": 2
+    "Permutation_impl_permutation": 1
+    "Permutation_in.": 2
+    "Permutation_ind_bis": 2
+    "Permutation_length": 2
+    "Permutation_length.": 1
+    "Permutation_length_1": 1
+    "Permutation_length_1_inv": 3
+    "Permutation_length_2": 1
+    "Permutation_length_2_inv": 2
+    "Permutation_map": 1
+    "Permutation_middle": 2
+    "Permutation_nil": 1
+    "Permutation_nil_app_cons": 1
+    "Permutation_nth_error": 2
+    "Permutation_rev": 3
+    "Permutation_trans": 1
+    "Playground1.": 5
     "Preliminary": 1
-    "Proof.": 6
+    "Proof": 18
+    "Proof.": 204
+    "Prop": 13
+    "Prop.": 1
+    "Proper": 5
     "Proving": 4
+    "Public": 4
     "Q": 3
-    "Qed.": 7
-    "Require": 3
-    "S": 7
+    "Q.": 2
+    "Qed": 24
+    "Qed.": 196
+    "R": 54
+    "Relations": 2
+    "Relations.": 1
+    "Require": 17
+    "Reserved": 3
+    "Resolve": 5
+    "S": 182
+    "S.": 1
+    "SCase": 24
+    "SCase.": 3
+    "SKIP": 3
+    "SLoad": 4
+    "SMinus": 9
+    "SMult": 9
+    "SPlus": 8
+    "SPush": 6
+    "SSCase": 5
+    "STLC.": 1
+    "ST_App1.": 2
+    "ST_App2": 1
+    "ST_App2.": 1
+    "ST_AppAbs.": 3
+    "ST_Funny": 1
+    "ST_If": 1
+    "ST_If.": 2
+    "ST_IfFalse": 1
+    "ST_IfFalse.": 1
+    "ST_IfTrue": 1
+    "ST_IfTrue.": 1
+    "ST_Plus1": 2
+    "ST_Plus1.": 2
+    "ST_Plus2.": 2
+    "ST_PlusConstConst": 3
+    "ST_PlusConstConst.": 3
+    "ST_ShortCut.": 1
+    "S_nbeq_0": 1
     "Scheme": 1
-    "Set": 1
+    "Section": 4
+    "Set": 4
+    "Setoid": 1
+    "SetoidList": 1
+    "SfLib.": 2
     "Showing": 3
+    "SimpleArith0.": 2
+    "SimpleArith1.": 2
+    "SimpleArith2.": 1
+    "SingletonBag": 4
     "Sketch": 1
-    "Theorem": 3
-    "Type": 2
-    "_": 18
-    "a": 7
-    "and": 1
-    "apply": 42
-    "as": 11
-    "assert": 13
-    "assumption": 2
-    "assumption.": 21
-    "at": 2
+    "Sn_le_Sm__n_le_m": 2
+    "Sn_le_Sm__n_le_m.": 1
+    "Some": 26
+    "Sorted": 5
+    "Sorted.": 1
+    "Sorted_inv": 2
+    "Sorting": 1
+    "Specification": 2
+    "T": 52
+    "T.": 9
+    "T0": 2
+    "T1": 25
+    "T11": 2
+    "T11.": 4
+    "T12": 2
+    "T2": 20
+    "T2.": 1
+    "T3": 2
+    "THEN": 3
+    "TODO": 2
+    "T_Abs.": 1
+    "T_App": 2
+    "T_Var.": 1
+    "Tactic": 10
+    "Team": 4
+    "Temp1.": 1
+    "Temp2.": 1
+    "Temp3.": 1
+    "Temp4.": 2
+    "Temp5.": 1
+    "Th": 1
+    "The": 10
+    "Theorem": 114
+    "This": 7
+    "Tree": 25
+    "Tree.": 1
+    "Tree_Leaf": 9
+    "Tree_Leaf.": 1
+    "Tree_Node": 11
+    "Trees": 1
+    "Treesort": 1
+    "True": 1
+    "Type": 91
+    "V": 6
+    "V1": 5
+    "V2": 4
+    "VV": 3
+    "VV/": 1
+    "Variable": 7
+    "Version": 4
+    "WHILE": 5
+    "We": 1
+    "X": 212
+    "X.": 4
+    "X0": 2
+    "XtimesYinZ": 1
+    "XtimesYinZ_spec": 1
+    "Y": 49
+    "Y.": 1
+    "Z": 24
+    "_": 68
+    "a": 231
+    "a*b": 1
+    "a.": 5
+    "a0": 13
+    "a0.": 1
+    "a1": 56
+    "a2": 59
+    "adapt": 4
+    "adapt.": 2
+    "adapt_injective": 1
+    "adapt_injective.": 1
+    "adapt_ok": 2
+    "adjacent": 1
+    "aeval": 44
+    "aexp": 37
+    "aexp.": 2
+    "aexp1": 1
+    "al": 3
+    "all3_spec": 1
+    "already": 1
+    "an": 3
+    "and": 7
+    "andb": 6
+    "andb3": 5
+    "andb_false_r": 1
+    "antisym": 1
+    "antisymmetric": 3
+    "app": 5
+    "app_ass": 1
+    "app_ass.": 6
+    "app_assoc": 2
+    "app_comm_cons": 3
+    "app_length": 2
+    "app_length.": 2
+    "app_nil_end": 1
+    "app_nil_end.": 1
+    "app_nil_r": 2
+    "apparatus": 1
+    "appears_free_in": 1
+    "apply": 325
+    "are": 2
+    "arith": 5
+    "arith.": 8
+    "as": 95
+    "assert": 55
+    "assertion": 3
+    "associativity": 10
+    "assumption": 3
+    "assumption.": 49
+    "at": 20
+    "auto": 77
+    "auto.": 48
+    "automatically": 2
+    "average": 1
     "axiom": 1
+    "b": 82
+    "b.": 9
+    "b1": 28
+    "b1.": 1
+    "b2": 23
+    "b3": 2
+    "bad": 1
+    "bag": 3
+    "base": 3
+    "based": 1
+    "basic": 1
+    "be": 2
+    "begin": 2
+    "beq_id": 13
+    "beq_id_eq": 5
+    "beq_id_false_not_eq.": 1
+    "beq_id_refl": 1
+    "beq_nat": 19
+    "beq_nat_O_l": 1
+    "beq_nat_O_r": 1
+    "beq_nat_eq": 1
+    "beq_nat_refl": 3
+    "beq_nat_sym": 1
+    "beq_natlist": 5
+    "beq_natlist_refl": 1
+    "between": 2
+    "beval": 12
+    "bexp": 22
+    "bexp.": 2
+    "bexp1": 1
+    "bin": 9
+    "bin.": 1
+    "bin2un": 3
+    "bin_comm": 1
+    "bind_option": 1
+    "bl": 3
+    "ble_n_Sn.": 1
+    "ble_nat": 5
+    "bogus": 1
+    "bool": 33
+    "bool.": 1
+    "bool_step_prop4": 1
+    "bool_step_prop4.": 2
+    "bool_step_prop4_holds": 1
     "bounded": 3
     "boundedness": 2
+    "break_list": 4
+    "build_heap": 3
     "building": 1
+    "but": 1
+    "by": 13
+    "c": 89
+    "c.": 2
+    "c1": 16
+    "c2": 11
+    "can": 1
     "card": 2
     "card_inj": 1
     "card_inj_aux": 1
@@ -5239,132 +5819,854 @@ tokens:
     "card_interval.": 2
     "cardinal": 1
     "cardinality": 4
-    "case": 4
+    "case": 5
+    "ceval__ceval_step": 3
+    "ceval__ceval_step.": 1
+    "ceval_and_ceval_step_coincide": 1
+    "ceval_cases": 1
+    "ceval_deterministic": 1
+    "ceval_example1": 1
+    "ceval_example2": 1
+    "ceval_step": 8
+    "ceval_step1": 3
+    "ceval_step2": 4
+    "ceval_step3": 5
+    "ceval_step__ceval": 1
+    "ceval_step__ceval.": 1
+    "ceval_step_more": 5
+    "change": 2
+    "characterization": 1
+    "clear": 11
+    "clos_refl_trans": 8
+    "com": 22
+    "com.": 1
+    "com_cases": 1
+    "combine": 3
+    "compatibilty": 1
+    "compatible": 2
+    "complex": 1
+    "complexity": 1
+    "composition": 1
+    "concerns": 1
     "conclude": 1
+    "congruence.": 1
+    "cons": 27
+    "cons_leA": 2
+    "cons_leA.": 2
+    "cons_sort": 2
+    "constfun": 1
+    "constructor": 4
+    "constructor.": 6
+    "contents": 15
+    "context": 2
+    "context_invariance...": 2
+    "contra.": 14
+    "contradict": 3
     "contradiction": 8
-    "decidable": 4
+    "contribution": 1
+    "corresponding": 1
+    "could": 1
+    "count": 7
+    "countoddmembers": 1
+    "curry_uncurry": 1
+    "d": 7
+    "dans": 1
+    "datatypes.": 47
+    "day": 9
+    "day.": 1
+    "decidable": 5
+    "decide": 1
+    "decide_left": 1
+    "define": 1
+    "defines": 1
+    "definition": 2
+    "defs": 1
+    "defs.": 1
     "dep_pair_intro": 2
     "dep_pair_intro.": 3
-    "destruct": 13
-    "discriminate": 2
-    "e": 2
-    "elements": 1
-    "else": 1
+    "dependent": 6
+    "deprecated": 2
+    "destruct": 87
+    "development": 1
+    "discriminate": 4
+    "discriminate.": 1
+    "distributed": 3
+    "do": 5
+    "domain": 1
+    "double": 2
+    "double_injective": 1
+    "e": 43
+    "e.": 7
+    "e1": 25
+    "e1.": 1
+    "e2": 27
+    "e3": 1
+    "eapply": 7
+    "eauto": 8
+    "eauto.": 7
+    "elements": 2
+    "elim": 21
+    "else": 13
+    "empty": 4
+    "emptyBag": 4
+    "empty_relation.": 1
+    "empty_relation_not_partial_funcion": 1
+    "empty_state": 13
+    "empty_state.": 1
+    "end": 16
+    "end.": 52
+    "eq": 4
+    "eq.": 11
+    "eq1": 6
+    "eq1.": 11
+    "eq2": 1
+    "eq2.": 9
+    "eqA": 29
+    "eqA_dec": 27
+    "eqA_dec.": 1
+    "eqA_equiv": 1
     "eq_S.": 1
+    "eq_add_S": 3
     "eq_nat_dec.": 1
     "eq_rect": 3
     "eq_rect_eq_nat": 2
     "eq_rect_eq_nat.": 1
-    "equality": 3
+    "equality": 6
+    "equipment": 1
+    "equiv_Tree": 1
+    "equivalence": 2
+    "equivalent": 1
     "et": 1
+    "eval": 9
+    "eval__stepmany": 1
+    "eval__value": 1
+    "eval_cases": 1
+    "evenb": 5
+    "every": 1
+    "ex_falso_quodlibet.": 1
+    "exact": 3
+    "execute_theorem": 1
+    "execute_theorem.": 1
+    "exfalso.": 1
     "exist": 7
-    "exists": 9
-    "f": 48
+    "exists": 49
+    "existsb": 3
+    "existsb2": 2
+    "existsb2.": 1
+    "existsb_correct": 1
+    "exp": 2
+    "extend": 1
+    "extend.": 2
+    "extend_neq": 1
+    "f": 132
+    "f.": 4
+    "f_equal": 1
+    "f_equal.": 1
+    "fact_body": 2
+    "fact_com": 1
+    "fact_loop": 1
+    "fact_loop.": 1
+    "factorial": 2
+    "false": 42
+    "false.": 11
+    "file": 6
+    "filter": 3
     "finite": 2
-    "for": 1
-    "forall": 12
-    "fun": 11
+    "first": 20
+    "fix": 2
+    "flat_exist": 3
+    "flat_spec": 3
+    "fmostlytrue": 5
+    "fold": 1
+    "fold_map": 2
+    "fold_map.": 1
+    "fold_map_correct": 1
+    "follows": 1
+    "for": 3
+    "forall": 226
+    "forallb": 4
+    "friday": 3
+    "from": 2
+    "fst": 3
+    "ftrue": 1
+    "fun": 19
     "functional": 1
-    "g": 7
-    "generalize": 4
-    "h": 2
+    "g": 9
+    "generalize": 13
+    "generated": 2
+    "grumble": 3
+    "gtA": 1
+    "h": 14
     "h.": 1
-    "has": 1
+    "h2": 1
+    "has": 2
+    "has_type": 4
+    "have": 1
     "having": 1
-    "if": 2
-    "in": 10
-    "induction": 1
+    "hd_opt": 8
+    "head": 1
+    "heap": 4
+    "heap_exist": 3
+    "heap_to_list": 2
+    "hide": 4
+    "holding": 1
+    "i": 31
+    "i1": 6
+    "i2": 14
+    "id": 10
+    "idB": 2
+    "idB.": 1
+    "idBB": 2
+    "idBBBB": 2
+    "ident": 10
+    "idtac": 1
+    "if": 16
+    "if_eqA": 1
+    "if_eqA_refl": 3
+    "if_eqA_rewrite_l": 1
+    "if_eqA_rewrite_r": 1
+    "if_eqA_then": 1
+    "iff": 2
+    "in": 157
+    "in_app_iff": 1
+    "in_map_iff": 1
+    "in_map_iff.": 2
+    "in_middle": 3
+    "in_or_app": 1
+    "in_seq": 4
+    "in_split": 1
+    "incbin": 2
+    "incl": 3
+    "index": 3
+    "index_okx": 1
+    "induction": 75
+    "initial": 1
     "inj_restrict": 1
-    "injection": 2
-    "injective": 1
+    "injection": 8
+    "injective": 6
+    "injective_bounded_surjective": 1
+    "injective_map_NoDup": 2
     "injectivity": 1
+    "insert": 2
+    "insert_exist": 4
+    "insert_spec": 3
+    "insertion": 1
+    "instead": 1
+    "intermediate": 1
     "interval": 3
     "interval_dec": 1
     "interval_dec.": 1
     "interval_discr": 1
-    "intro": 16
+    "into": 2
+    "intro": 28
     "introduce": 1
-    "intros": 13
-    "intros.": 2
+    "intros": 228
+    "intros.": 28
+    "intuition": 1
+    "intuition.": 2
+    "inversion": 95
+    "inversion_clear": 6
+    "invert_heap": 3
     "irrelevance": 2
-    "is": 10
-    "l": 3
-    "l0": 1
-    "le": 1
+    "is": 22
+    "is_heap": 18
+    "is_heap_rec": 1
+    "is_heap_rect": 1
+    "it": 1
+    "j": 6
+    "j.": 1
+    "just": 1
+    "k": 7
+    "k1": 20
+    "k1.": 1
+    "k2": 21
+    "k2.": 1
+    "k3": 6
+    "k3.": 1
+    "l": 378
+    "l.": 26
+    "l0": 7
+    "l1": 104
+    "l1.": 5
+    "l2": 86
+    "l2.": 10
+    "l3": 12
+    "l3.": 1
+    "l4": 3
+    "le": 3
+    "le.": 3
+    "leA": 27
+    "leA_Tree": 16
+    "leA_Tree_Leaf": 5
+    "leA_Tree_Node": 1
+    "leA_antisym": 1
+    "leA_antisym.": 1
+    "leA_dec": 4
+    "leA_refl": 1
+    "leA_refl.": 1
+    "leA_trans": 2
     "le_O_n.": 2
-    "le_S": 5
-    "le_Sn_le": 1
-    "le_Sn_n": 4
+    "le_S": 6
+    "le_S.": 4
+    "le_S_n": 2
+    "le_Sn_le": 2
+    "le_Sn_n": 5
+    "le_antisymmetric": 2
     "le_ind": 1
-    "le_lt_dec": 4
+    "le_lt_dec": 9
     "le_lt_trans": 2
     "le_n": 4
+    "le_n.": 6
     "le_n_O_eq.": 2
     "le_n_S": 1
     "le_neq_lt": 2
+    "le_not_a_partial_function": 1
     "le_not_lt": 1
+    "le_order": 1
+    "le_reflexive": 2
+    "le_step": 1
+    "le_trans": 5
     "le_uniqueness_proof": 1
-    "left.": 1
-    "let": 1
+    "left": 8
+    "left.": 3
+    "lemma": 3
+    "length": 23
+    "length.": 1
+    "let": 4
+    "level": 14
+    "list": 77
+    "list.": 1
+    "list123": 1
+    "list_contents": 30
+    "list_contents_app": 5
+    "list_contents_app.": 1
+    "list_to_heap": 2
+    "lists": 6
+    "lists.": 1
+    "log": 1
+    "loop": 1
+    "loop_never_stops": 1
+    "low_trans": 3
+    "lower": 1
+    "lt": 3
+    "lt.": 2
     "lt_O_neq": 2
     "lt_irrefl": 2
     "lt_le_trans": 1
     "lt_n_Sn.": 1
-    "lt_trans": 1
-    "m": 27
-    "m.": 1
+    "lt_trans": 4
+    "lx": 4
+    "ly": 4
+    "m": 196
+    "m.": 19
     "m0": 1
-    "n": 49
-    "n.": 2
+    "m1": 1
+    "m2.": 1
+    "map": 4
+    "map_length": 1
+    "map_length.": 1
+    "match": 71
+    "meq": 15
+    "meq.": 2
+    "meq_congr": 1
+    "meq_congr.": 1
+    "meq_left": 1
+    "meq_right": 2
+    "meq_singleton": 1
+    "meq_sym": 2
+    "meq_trans": 10
+    "meq_trans.": 1
+    "merge": 5
+    "merge0": 1
+    "merge0.": 2
+    "merge_exist": 5
+    "merge_lem": 3
+    "minus": 3
+    "minustwo": 1
+    "monday": 5
+    "more": 1
+    "mult": 3
+    "mult_0_plus": 1
+    "mult_0_r.": 4
+    "mult_1": 1
+    "mult_1.": 1
+    "mult_1_1": 1
+    "mult_1_distr.": 1
+    "mult_1_plus": 1
+    "mult_assoc": 1
+    "mult_comm": 2
+    "mult_distr": 1
+    "mult_mult": 1
+    "mult_mult.": 3
+    "mult_plus_1": 1
+    "mult_plus_1.": 1
+    "mult_plus_distr_r": 1
+    "mult_plus_distr_r.": 1
+    "multiplicity": 8
+    "multiplicity_InA": 4
+    "multiplicity_InA.": 1
+    "multiplicity_InA_O": 2
+    "multiplicity_InA_S": 1
+    "multiplicity_NoDupA": 1
+    "multiset": 4
+    "multisets": 4
+    "mumble": 5
+    "mumble.": 1
+    "munion": 18
+    "munion_ass": 1
+    "munion_ass.": 2
+    "munion_comm": 1
+    "munion_comm.": 2
+    "munion_rotate.": 1
+    "must": 1
+    "n": 358
+    "n.": 38
     "n0": 4
-    "nat": 18
+    "n1": 19
+    "n2": 15
+    "nandb": 5
+    "nat": 99
+    "nat.": 3
+    "nat_bijection_Permutation": 1
+    "nat_scope.": 3
+    "natlist": 7
+    "natoption": 5
+    "natoption.": 1
+    "natprod": 5
+    "natprod.": 1
+    "negb": 9
     "neq_dep_intro": 2
-    "notion": 1
-    "of": 10
-    "on": 7
-    "p": 41
+    "next_nat": 1
+    "next_nat.": 1
+    "next_nat_closure_is_le": 1
+    "next_nat_partial_function": 1
+    "next_weekday": 3
+    "nf_same_as_value": 3
+    "nil": 41
+    "nil.": 1
+    "nil_app": 1
+    "nil_is_heap": 5
+    "nil_is_heap.": 1
+    "nn.": 1
+    "node_is_heap": 7
+    "normal_form": 4
+    "normal_form.": 3
+    "normal_form_of.": 2
+    "normal_forms_unique": 1
+    "normalizing": 1
+    "not": 2
+    "not.": 3
+    "notations": 1
+    "notion": 2
+    "now": 19
+    "nth": 2
+    "nth_error": 7
+    "nth_error_None": 4
+    "nth_error_app1": 1
+    "nth_error_app2": 1
+    "nx": 1
+    "ny": 1
+    "o": 20
+    "o.": 3
+    "oddb": 5
+    "of": 32
+    "omega": 2
+    "omega.": 6
+    "on": 10
+    "only": 3
+    "optimize_0plus": 10
+    "optimize_0plus_sound": 2
+    "option": 10
+    "option_elim": 2
+    "option_elim_hd": 1
+    "or": 1
+    "orb": 8
+    "order": 3
+    "ordered": 1
+    "other": 20
+    "other.": 4
+    "ought": 2
+    "over": 1
+    "override": 5
+    "override.": 2
+    "override_eq": 1
+    "override_example": 1
+    "override_example1": 1
+    "override_example2": 1
+    "override_example3": 1
+    "override_example4": 1
+    "override_neq": 1
+    "p": 93
+    "p.": 9
+    "pair": 7
+    "parsing": 3
+    "partial_function": 7
+    "partial_function.": 6
+    "partial_map": 4
+    "particular": 1
     "pattern": 2
+    "perm_nil": 1
+    "perm_skip": 1
+    "perm_trans": 1
+    "permut_InA_InA": 3
+    "permut_add_cons_inside": 3
+    "permut_add_cons_inside.": 1
+    "permut_add_inside": 1
+    "permut_add_inside_eq": 1
+    "permut_app": 1
+    "permut_app_inv1": 1
+    "permut_cons": 5
+    "permut_cons_InA": 4
+    "permut_cons_eq": 3
+    "permut_conv_inv": 1
+    "permut_eqA": 1
+    "permut_length": 1
+    "permut_length_1": 1
+    "permut_length_1.": 2
+    "permut_length_2": 1
+    "permut_middle": 1
+    "permut_nil": 2
+    "permut_refl": 1
+    "permut_refl.": 5
+    "permut_remove_hd": 1
+    "permut_remove_hd_eq": 1
+    "permut_rev": 1
+    "permut_right": 1
+    "permut_sym": 3
+    "permut_sym_app": 1
+    "permut_tran": 1
+    "permut_trans": 4
+    "permutation": 47
+    "permutation.": 1
+    "permutation_Permutation": 2
+    "permutations": 1
+    "plus": 10
+    "plus2": 1
+    "plus2_spec": 1
+    "plus3": 2
+    "plus3.": 1
+    "plus_0_r.": 1
+    "plus_1_1.": 1
+    "plus_1_neq_0": 1
+    "plus_O_n": 1
+    "plus_O_n.": 1
+    "plus_assoc": 1
+    "plus_assoc.": 4
+    "plus_ble_compat_1": 1
+    "plus_comm": 3
+    "plus_comm.": 3
+    "plus_distr.": 1
+    "plus_n_Sm": 1
+    "plus_n_Sm.": 1
+    "plus_rearrange": 1
+    "plus_reg_l": 1
+    "plus_reg_l.": 1
+    "plus_swap": 2
+    "plus_swap.": 2
     "pose": 1
-    "pred": 1
+    "postulate": 1
+    "power": 2
+    "prealable.": 1
+    "pred": 3
     "pred_inj.": 1
     "preliminary": 1
+    "preorder": 1
+    "preservation": 1
+    "prod": 3
+    "prod_curry": 3
+    "prod_uncurry": 3
     "proj1_sig": 1
     "proj2_sig": 1
     "proof": 1
     "proofs": 3
+    "properties": 1
+    "property": 1
     "prove": 3
-    "q": 8
-    "q.": 1
+    "q": 15
+    "q.": 2
+    "r": 10
+    "r.": 2
+    "r1": 3
+    "r1.": 1
+    "r2": 2
+    "red": 7
+    "red.": 1
+    "refl": 1
     "refl_equal": 4
-    "reflexivity.": 8
-    "relation": 1
-    "replace": 2
-    "results": 2
-    "rewrite": 18
-    "right.": 3
-    "set": 1
+    "refl_step_closure": 11
+    "reflexive": 5
+    "reflexive.": 1
+    "reflexivity": 14
+    "reflexivity.": 180
+    "relation": 21
+    "relations": 1
+    "remember": 9
+    "remove_all": 2
+    "remove_decreases_count": 1
+    "remove_one": 3
+    "rename": 2
+    "repeat": 9
+    "replace": 4
+    "requires": 1
+    "results": 3
+    "rev": 7
+    "rev_exercise": 1
+    "rev_involutive.": 1
+    "rev_snoc": 1
+    "revert": 5
+    "rewrite": 223
+    "right": 7
+    "right.": 9
+    "rsc_R": 2
+    "rsc_refl": 1
+    "rsc_refl.": 4
+    "rsc_step": 4
+    "rsc_step.": 2
+    "rsc_trans": 4
+    "rt_refl": 1
+    "rt_refl.": 2
+    "rt_step": 1
+    "rt_step.": 2
+    "rt_trans": 3
+    "rtc_rsc_coincide": 1
+    "ry": 1
+    "s": 12
+    "s.": 5
+    "s1": 20
+    "s2": 2
+    "s_compile": 36
+    "s_compile1": 1
+    "s_compile_correct": 1
+    "s_execute": 21
+    "s_execute1": 1
+    "s_execute2": 1
+    "same": 1
+    "sans": 1
+    "saturday": 3
+    "seq": 2
+    "seq_NoDup": 1
+    "seq_NoDup.": 1
+    "set": 3
+    "setoid_rewrite": 2
     "sets": 1
-    "simpl.": 2
-    "split.": 3
+    "short": 1
+    "shows": 1
+    "silly1": 1
+    "silly2a": 1
+    "silly3": 1
+    "silly4": 1
+    "silly5": 1
+    "silly6": 1
+    "silly7": 1
+    "silly_ex": 1
+    "sillyex1": 1
+    "sillyex2": 1
+    "simpl": 66
+    "simpl.": 72
+    "simple": 7
+    "singletonBag": 10
+    "sinstr": 2
+    "skip": 1
+    "snd": 3
+    "snoc": 9
+    "snoc_with_append": 1
+    "sorted": 4
+    "specialize": 6
+    "split": 17
+    "split.": 10
+    "st": 132
+    "st.": 2
+    "st1": 6
+    "st2": 3
+    "st2.": 1
+    "state": 13
+    "step": 9
+    "step.": 3
+    "step_cases": 4
+    "step_deterministic": 1
+    "step_example3": 1
+    "step_normal_form": 1
+    "step_normal_form.": 1
+    "stepmany": 4
+    "stepmany.": 1
+    "stepmany_congr2": 1
+    "stepmany_congr_1": 1
+    "strong_progress": 2
+    "subst": 10
+    "subst.": 37
+    "substitution_preserves_typing": 1
+    "subtract_3_from_5_slowly": 1
+    "subtract_slowly": 1
+    "subtract_slowly.": 1
+    "subtract_slowly_body": 2
+    "sunday": 2
+    "supply": 1
     "surjective": 2
+    "surjective_pairing": 1
     "surjectivity": 1
+    "swap_pair": 1
     "sym_not_eq.": 2
-    "symmetry": 1
-    "that": 7
-    "the": 6
-    "then": 1
-    "trivial.": 1
-    "unfold": 5
+    "symmetric": 2
+    "symmetry": 5
+    "symmetry.": 2
+    "t": 96
+    "t.": 4
+    "t1": 48
+    "t2": 51
+    "t2.": 4
+    "t3": 6
+    "t3.": 2
+    "t_false": 1
+    "t_true": 1
+    "tactic": 10
+    "take": 1
+    "tauto": 1
+    "tauto.": 1
+    "terms": 3
+    "test": 4
+    "test_aeval1": 1
+    "test_andb31": 1
+    "test_andb32": 1
+    "test_andb33": 1
+    "test_andb34": 1
+    "test_beq_natlist1": 1
+    "test_beq_natlist2": 1
+    "test_factorial1": 1
+    "test_hd_opt1": 2
+    "test_hd_opt2": 2
+    "test_nandb1": 1
+    "test_nandb2": 1
+    "test_nandb3": 1
+    "test_nandb4": 1
+    "test_next_weekday": 1
+    "test_oddb1": 1
+    "test_oddb2": 1
+    "test_optimize_0plus": 1
+    "test_orb1": 1
+    "test_orb2": 1
+    "test_orb3": 1
+    "test_orb4": 1
+    "test_remove_one1": 1
+    "test_repeat1": 1
+    "test_step_1": 1
+    "test_step_2": 1
+    "than": 2
+    "that": 8
+    "the": 24
+    "then": 12
+    "there": 1
+    "this": 2
+    "thursday": 3
+    "tl": 7
+    "tm": 43
+    "tm.": 3
+    "tm_abs": 9
+    "tm_app": 7
+    "tm_cases": 1
+    "tm_const": 45
+    "tm_false": 5
+    "tm_false.": 3
+    "tm_if": 10
+    "tm_plus": 30
+    "tm_true": 8
+    "tm_var": 6
+    "to": 6
+    "tools": 2
+    "total": 2
+    "total_relation": 1
+    "total_relation1.": 2
+    "total_relation_not_partial_function": 1
+    "tp": 2
+    "transitive": 9
+    "transitive.": 1
+    "transitivity": 4
+    "transpositions": 1
+    "tree": 2
+    "trees": 5
+    "treesort": 2
+    "treesort_twist1": 1
+    "treesort_twist2": 1
+    "trivial": 13
+    "trivial.": 14
+    "true": 52
+    "true.": 17
+    "try": 10
+    "tuesday": 3
+    "tuesday.": 1
+    "two": 5
+    "tx": 2
+    "ty": 7
+    "ty.": 2
+    "ty_Bool": 10
+    "ty_Bool.": 1
+    "ty_arrow": 7
+    "type_scope.": 1
+    "types_unique": 1
+    "un": 2
+    "uncurry_uncurry": 1
+    "under": 3
+    "unfold": 67
+    "unfold_example_bad": 1
     "unicity": 1
+    "update": 28
+    "update.": 3
+    "update_eq": 1
+    "update_eq.": 2
+    "update_example": 1
+    "update_neq": 1
+    "update_permute": 1
+    "update_same": 1
+    "update_shadow": 1
+    "use": 3
+    "used.": 1
+    "uses": 1
+    "using": 17
+    "v": 37
+    "v.": 2
+    "v1": 7
+    "v2": 2
+    "v_abs": 1
+    "v_abs.": 2
+    "v_const": 4
+    "v_const.": 1
+    "v_false": 1
+    "v_funny.": 1
+    "v_true": 1
+    "value": 25
+    "value.": 1
+    "value_not_same_as_normal_form": 2
+    "via": 1
+    "we": 2
+    "wednesday": 3
+    "what": 1
+    "where": 5
+    "which": 1
     "while": 1
-    "with": 9
-    "x": 75
+    "with": 216
+    "worst": 1
+    "x": 260
+    "x.": 5
+    "x0": 8
+    "x0.": 1
+    "x1": 17
+    "x1.": 1
+    "x2": 14
     "x=": 1
     "xSn": 28
-    "y": 24
-    "{": 15
-    "|": 27
-    "}": 10
+    "xo": 2
+    "xs": 7
+    "y": 123
+    "y.": 14
+    "y1": 7
+    "y2": 6
+    "y2.": 4
+    "z": 14
+    "z.": 6
+    "zero_nbeq_S": 1
+    "{": 36
+    "|": 398
+    "||": 2
+    "}": 29
   "Dart":
     "(": 7
     ")": 7
@@ -18004,32 +19306,427 @@ tokens:
     "std_logic": 2
     "use": 1
   "Verilog":
-    "&": 3
-    "(": 11
-    ")": 11
-    "*/": 1
-    "/*": 1
-    ";": 26
-    "assign": 8
+    "#": 10
+    "#0.1": 8
+    "#1": 1
+    "#10": 10
+    "#100": 1
+    "#1000": 1
+    "#10000": 1
+    "#5": 3
+    "#50": 2
+    "%": 3
+    "&": 6
+    "&&": 3
+    "(": 372
+    ")": 371
+    "*": 5
+    "*/": 4
+    "+": 36
+    "-": 71
+    ".BITS": 1
+    ".C": 6
+    ".CE": 6
+    ".CLK_FREQUENCY": 1
+    ".D": 6
+    ".DEBOUNCE_HZ": 1
+    ".INIT": 6
+    ".INPUT_BITS": 1
+    ".Q": 6
+    ".R": 6
+    ".S": 6
+    ".bitmask": 2
+    ".button": 1
+    ".chain_four": 2
+    ".clk": 6
+    ".clk_i": 1
+    ".color_compare": 2
+    ".color_dont_care": 2
+    ".command_was_sent": 1
+    ".csr_adr_i": 1
+    ".csr_adr_o": 1
+    ".csr_dat_i": 1
+    ".csr_dat_o": 1
+    ".csr_stb_i": 1
+    ".csr_stb_o": 1
+    ".csrm_adr_o": 1
+    ".csrm_dat_i": 1
+    ".csrm_dat_o": 1
+    ".csrm_sel_o": 1
+    ".csrm_we_o": 1
+    ".cur_end": 2
+    ".cur_start": 2
+    ".dac_read_data": 2
+    ".dac_read_data_cycle": 2
+    ".dac_read_data_register": 2
+    ".dac_we": 2
+    ".dac_write_data": 2
+    ".dac_write_data_cycle": 2
+    ".dac_write_data_register": 2
+    ".data_valid": 2
+    ".debounce": 1
+    ".div_by_zero": 1
+    ".dividend": 1
+    ".divisor": 1
+    ".en": 4
+    ".enable_set_reset": 2
+    ".end_hor_retr": 2
+    ".end_horiz": 2
+    ".end_ver_retr": 2
+    ".end_vert": 2
+    ".error_communication_timed_out": 1
+    ".graphics_alpha": 2
+    ".hcursor": 2
+    ".horiz_sync": 1
+    ".horiz_total": 2
+    ".map_mask": 2
+    ".memory_mapping1": 2
+    ".num": 4
+    ".pal_addr": 2
+    ".pal_read": 2
+    ".pal_we": 2
+    ".pal_write": 2
+    ".ps2_clk": 1
+    ".ps2_clk_negedge": 2
+    ".ps2_clk_posedge": 2
+    ".ps2_dat": 1
+    ".ps2_data": 1
+    ".quotient": 1
+    ".radicand": 1
+    ".raster_op": 2
+    ".read_map_select": 2
+    ".read_mode": 2
+    ".received_data": 1
+    ".received_data_en": 1
+    ".reset": 2
+    ".reset_n": 3
+    ".root": 1
+    ".rst": 1
+    ".rst_i": 1
+    ".seg": 4
+    ".send_command": 1
+    ".set_reset": 2
+    ".shift_reg1": 2
+    ".st_hor_retr": 2
+    ".st_ver_retr": 2
+    ".start": 2
+    ".start_addr": 1
+    ".start_receiving_data": 1
+    ".the_command": 1
+    ".v_retrace": 2
+    ".vcursor": 2
+    ".vert_sync": 1
+    ".vert_total": 2
+    ".vga_blue_o": 1
+    ".vga_green_o": 1
+    ".vga_red_o": 1
+    ".vh_retrace": 2
+    ".wait_for_incoming_data": 1
+    ".wb_ack_o": 2
+    ".wb_adr_i": 2
+    ".wb_clk_i": 2
+    ".wb_dat_i": 2
+    ".wb_dat_o": 2
+    ".wb_rst_i": 2
+    ".wb_sel_i": 2
+    ".wb_stb_i": 2
+    ".wb_we_i": 2
+    ".wbm_ack_i": 1
+    ".wbm_adr_o": 1
+    ".wbm_dat_i": 1
+    ".wbm_dat_o": 1
+    ".wbm_sel_o": 1
+    ".wbm_stb_o": 1
+    ".wbm_we_o": 1
+    ".wbs_ack_o": 1
+    ".wbs_adr_i": 1
+    ".wbs_dat_i": 1
+    ".wbs_dat_o": 1
+    ".wbs_sel_i": 1
+    ".wbs_stb_i": 1
+    ".wbs_we_i": 1
+    ".write_mode": 2
+    ".x_dotclockdiv2": 2
+    "/": 11
+    "/*": 4
+    "//": 369
+    "////////////////////////////////////////////////////////////////////////////////": 14
+    "1": 7
+    ";": 287
+    "<": 47
+    "<<": 2
+    "<=>": 4
+    "@": 16
+    "BITS": 2
+    "BIT_WIDTH": 5
+    "BIT_WIDTH*": 5
+    "BIT_WIDTH*i": 2
+    "CLK_FREQUENCY": 4
+    "COUNT": 4
+    "COUNT_VALUE": 2
+    "DEBOUNCE_HZ": 4
+    "DFF0": 1
+    "DFF10": 1
+    "DFF2": 1
+    "DFF4": 1
+    "DFF6": 1
+    "DFF8": 1
+    "FDRSE": 6
+    "FIRE": 4
+    "INPUT_BITS": 28
+    "INPUT_BITS*": 27
+    "INPUT_BITS*i": 5
+    "INPUT_WIDTH": 5
+    "NUMBER_OF_STAGES": 7
+    "OUTPUT_BITS": 14
+    "OUTPUT_BITS*INPUT_BITS": 9
+    "OUTPUT_WIDTH": 4
+    "PS2_STATE_0_IDLE": 10
+    "PS2_STATE_1_DATA_IN": 3
+    "PS2_STATE_2_COMMAND_OUT": 2
+    "PS2_STATE_3_END_TRANSFER": 3
+    "PS2_STATE_4_END_DELAYED": 4
+    "WAIT": 6
+    "a": 3
+    "always": 23
+    "an": 6
+    "assign": 23
+    "b": 3
+    "b0": 27
+    "b0000": 1
+    "b01": 1
+    "b1": 13
+    "b11": 1
+    "begin": 46
+    "bitmask": 3
+    "button": 24
+    "button_debounce": 3
+    "bx": 4
+    "c": 3
+    "case": 3
     "ch": 1
+    "chain_four": 3
+    "clk": 40
+    "color_compare": 3
+    "color_dont_care": 3
+    "command_was_sent": 2
+    "conf_wb_ack_o": 3
+    "conf_wb_dat_o": 3
+    "config_iface": 1
+    "control": 1
+    "count": 6
+    "cout": 4
+    "cpu_mem_iface": 1
+    "csr_adr_i": 3
+    "csr_adr_o": 2
+    "csr_dat_i": 3
+    "csr_stb_i": 2
+    "csr_stb_o": 3
+    "csrm_adr_o": 2
+    "csrm_dat_i": 2
+    "csrm_dat_o": 2
+    "csrm_sel_o": 2
+    "csrm_we_o": 2
+    "cur_end": 3
+    "cur_start": 3
+    "d": 3
+    "dac_read_data": 3
+    "dac_read_data_cycle": 3
+    "dac_read_data_register": 3
+    "dac_we": 3
+    "dac_write_data": 3
+    "dac_write_data_cycle": 3
+    "dac_write_data_register": 3
+    "data_valid": 7
+    "debounce": 6
+    "default": 2
+    "div_by_zero": 2
+    "div_pipelined": 2
+    "dividend": 3
+    "divisor": 5
+    "dsp_sel": 9
+    "e": 3
     "e0": 1
     "e1": 1
-    "endmodule": 6
-    "input": 6
+    "else": 22
+    "en": 13
+    "enable_set_reset": 3
+    "end": 48
+    "end_hor_retr": 3
+    "end_horiz": 3
+    "end_ver_retr": 3
+    "end_vert": 3
+    "endcase": 3
+    "endgenerate": 3
+    "endmodule": 18
+    "error_communication_timed_out": 3
+    "f": 2
+    "finish": 2
+    "for": 4
+    "g": 2
+    "gen_sign_extend": 1
+    "generate": 3
+    "genvar": 3
+    "graphics_alpha": 4
+    "h": 2
+    "h00": 1
+    "h01": 1
+    "h1": 1
+    "h3": 1
+    "hcursor": 3
+    "hex0": 2
+    "hex1": 2
+    "hex2": 2
+    "hex3": 2
+    "hex_display": 1
+    "hex_group0": 1
+    "hex_group1": 1
+    "hex_group2": 1
+    "hex_group3": 1
+    "horiz_sync": 2
+    "horiz_total": 3
+    "i": 60
+    "i/2": 2
+    "idle_counter": 4
+    "if": 23
+    "initial": 3
+    "inout": 2
+    "input": 37
+    "j": 2
+    "k": 2
+    "l": 2
+    "last_ps2_clk": 4
+    "lcd": 1
+    "localparam": 4
     "maj": 1
-    "module": 6
-    "ns/1ps": 1
+    "map_mask": 3
+    "mask_4": 1
+    "mask_gen": 9
+    "mem_arbitrer": 1
+    "mem_wb_ack_o": 3
+    "mem_wb_dat_o": 3
+    "memory_mapping1": 3
+    "module": 18
+    "mouse_cmdout": 1
+    "mouse_datain": 1
+    "mux": 1
+    "negedge": 8
+    "next_state": 6
+    "ns": 8
+    "ns/1ps": 2
+    "ns_ps2_transceiver": 13
+    "num": 5
     "o": 6
-    "output": 6
+    "opA": 4
+    "opB": 3
+    "or": 14
+    "original": 3
+    "out": 5
+    "output": 35
+    "pal_addr": 3
+    "pal_read": 3
+    "pal_we": 3
+    "pal_write": 3
+    "parameter": 7
+    "pipe_gen": 6
+    "pipe_in": 4
+    "pipe_out": 5
+    "pipeline": 2
+    "pipeline_registers": 1
+    "pipeline_stage": 1
+    "posedge": 11
+    "ps": 8
+    "ps2_clk": 3
+    "ps2_clk_negedge": 3
+    "ps2_clk_posedge": 3
+    "ps2_clk_reg": 4
+    "ps2_dat": 3
+    "ps2_data_reg": 5
+    "ps2_mouse": 1
+    "ps2_mouse_cmdout": 1
+    "ps2_mouse_datain": 1
+    "quotient": 2
+    "quotient_correct": 1
+    "radicand": 10
+    "radicand_gen": 10
+    "raster_op": 3
+    "read_map_select": 3
+    "read_mode": 3
+    "received_data": 2
+    "received_data_en": 4
+    "reg": 26
+    "reset": 5
+    "reset_n": 32
+    "root": 6
+    "root_gen": 15
     "s0": 1
     "s1": 1
-    "timescale": 1
+    "s_ps2_transceiver": 8
+    "seg_7": 4
+    "send_command": 2
+    "set_reset": 3
+    "shift_reg1": 3
+    "sign_extend": 3
+    "sign_extended_original": 2
+    "sign_extender": 1
+    "sqrt_pipelined": 3
+    "st_hor_retr": 3
+    "st_ver_retr": 3
+    "start": 11
+    "start_addr": 2
+    "start_gen": 7
+    "start_receiving_data": 3
+    "state": 6
+    "stb": 4
+    "sum": 5
+    "t_button_debounce": 1
+    "t_div_pipelined": 1
+    "t_sqrt_pipelined": 1
+    "the_command": 2
+    "timescale": 10
+    "v_retrace": 3
+    "vcursor": 3
+    "vert_sync": 2
+    "vert_total": 3
+    "vga": 1
+    "vga_blue_o": 2
+    "vga_config_iface": 1
+    "vga_cpu_mem_iface": 1
+    "vga_green_o": 2
+    "vga_lcd": 1
+    "vga_mem_arbitrer": 1
+    "vga_red_o": 2
+    "vh_retrace": 3
+    "w_vert_sync": 3
+    "wait_for_incoming_data": 3
+    "wb_ack_o": 2
+    "wb_adr_i": 3
+    "wb_clk_i": 6
+    "wb_cyc_i": 2
+    "wb_dat_i": 3
+    "wb_dat_o": 2
+    "wb_rst_i": 6
+    "wb_sel_i": 3
+    "wb_stb_i": 2
+    "wb_tga_i": 5
+    "wb_we_i": 3
+    "wbm_ack_i": 3
+    "wbm_adr_o": 3
+    "wbm_dat_i": 3
+    "wbm_dat_o": 3
+    "wbm_sel_o": 3
+    "wbm_stb_o": 3
+    "wbm_we_o": 3
+    "wire": 67
+    "write_mode": 3
     "x": 41
+    "x_dotclockdiv2": 3
     "y": 21
     "z": 7
-    "{": 10
+    "{": 11
     "|": 2
-    "}": 10
+    "||": 1
+    "}": 11
   "VimL":
     "-": 1
     "T": 1