Lines Matching refs:word
51 <| RFR : bool; NSASEDIS : bool; NSD32DIS : bool; cp : 14 word |>`;
141 `align (w : 'a word, n : num) : 'a word = n2w (n * (w2n w DIV n))`;
144 aligned (w : 'a word, n : num) = (w = align(w,n))`;
147 count_leading_zeroes (w : 'a word) =
154 lowest_set_bit (w : 'a word) =
184 signed_sat_q (i:int, N:num) : ('a word # bool) =
196 unsigned_sat_q (i:int, N:num) : ('a word # bool) =
211 LSL_C (x: 'a word, shift:num) =
219 LSR_C (x: 'a word, shift:num) =
226 ASR_C (x: 'a word, shift:num) =
233 ROR_C (x: 'a word, shift:num) =
240 RRX_C (x: 'a word, carry_in:bool) =
244 val LSL_def = Define `LSL (x: 'a word, shift:num) = x << shift`;
245 val LSR_def = Define `LSR (x: 'a word, shift:num) = x >>> shift`;
246 val ASR_def = Define `ASR (x: 'a word, shift:num) = x >> shift`;
247 val ROR_def = Define `ROR (x: 'a word, shift:num) = x #>> shift`;
250 RRX (x: 'a word, carry_in:bool) = SND (word_rrx (carry_in,x))`;
360 `!n a:'a word. align (a,2 ** n) = (dimindex(:'a) - 1 '' n) a`,
380 `!i n. i < dimindex (:'a) ==> ((n2w n : 'a word) ' i = BIT i n)`,
408 `!w. lowest_set_bit (w:'a word) =