Lines Matching refs:word
1131 val word_index_def = Define `word_index (w:'a word) n = w ' n`;
1132 val w2w_itself_def = Define `w2w_itself (:'a) w = (w2w w): 'a word`;
1133 val sw2sw_itself_def = Define `sw2sw_itself (:'a) w = (sw2sw w): 'a word`;
1134 val word_eq_def = Define `word_eq (v: 'a word) w = (v = w)`;
1159 `!b. $FCP (K b) = n2w (if b then 1 else 0) : 1 word`,
1219 val w = "type word" ^ x ^ " = " ^ s ^ " word"
1225 "val toWord" ^ x ^ " : NumML.num -> word" ^ x,
1231 "val toWord" ^ x ^ " : numML.num -> word" ^ x,
1233 " = o(toWord" ^ x ^ ", numML.fromString) : string -> word" ^ x)
1234 val d = "val fromString" ^ x ^ " : string -> word" ^ x
1273 :: MLSIG "datatype 'a word = n2w_itself of num * 'a itself"
1274 :: MLSTRUCT "datatype 'a word = n2w_itself of num * 'a itself"
1284 "type 'a word = N2w_itself of num * 'a itself"] @
1334 val i2w_itself_def = Define `i2w_itself(i,(:'a)) = i2w i : 'a word`;
1434 :: MLSIG "type 'a word = 'a wordsML.word"
1470 "type 'a word = 'a WordsML.word"]