diff --git a/lib/linguist/classifier.yml b/lib/linguist/classifier.yml index a3f051c6..2e314ee9 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 + "": 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