Lines Matching refs:word
3 (* DESCRIPTION : Support for maps 'a word |-> 'b and string |-> 'a *)
75 PEEKw (t:('a,'b) word_ptree) (w:'a word) = PEEK (THE_PTREE t) (w2n w)`;
80 ADDw (t:('a,'b) word_ptree) (w:'a word,d) =
86 REMOVEw (t:('a,'b) word_ptree) (w:'a word) =
96 MAP (n2w:num->'a word) (TRAVERSE (THE_PTREE t))`;
106 EVERY_LEAF (\k d. P (n2w k : 'a word) d) (THE_PTREE t)`;
110 EXISTS_LEAF (\k d. P (n2w k : 'a word) d) (THE_PTREE t)`;
116 `$IN_PTREEw (w:'a word) (t:('a,unit) word_ptree) =
120 `$INSERT_PTREEw (w:'a word) (t:('a,unit) word_ptree) =
131 PTREE_OF_WORDSET (t:('a, unit) word_ptree) (s:'a word set) =