Lines Matching refs:word
17 val align_def = Define `align p (w: 'a word) = (dimindex (:'a) - 1 '' p) w`
21 byte_align (w: 'a word) = align (LOG2 (dimindex(:'a) DIV 8)) w`
24 byte_aligned (w: 'a word) = aligned (LOG2 (dimindex(:'a) DIV 8)) w`
89 `(p - 1 >< 0) w : 'a word = (dimindex (:'a) - 1 >< 0) w`
104 !p w. aligned p (w: 'a word) <=> (p = 0) \/ ((p - 1 >< 0) w = 0w: 'a word)
130 `!p w:'a word. dimindex(:'a) <= p ==> (aligned p w = (w = 0w))`,
135 `!p w. aligned p (w: 'a word) = (w && n2w (2 ** p - 1) = 0w)`,
150 aligned p (w: 'a word) = (bit_count_upto (MIN (dimindex(:'a)) p) w = 0)`,
165 `!p a: 'a word b.
184 `!p a: 'a word b.
190 `!p w: 'a word. aligned p (1w << p * w)`,
199 \\ `(n >< 0) ((1w:'a word) << SUC n) = 0w: 'a word`
209 `!p w: 'a word x.
226 `!p a b : 'a word.
266 aligned k w <=> (w2n (w:'a word) MOD 2 ** k = 0)
307 dimindex (:'a) <= k ==> (n2w (2 ** k) = 0w:'a word)
323 p < dimindex(:'a) ==> (word_msb (align p w) = word_msb (w:'a word))
570 wordsLib.WORD_DECIDE ``a + (b * c + d) : 'a word = (a + d) + b * c``,
571 wordsLib.WORD_DECIDE ``a - (b * c + d) : 'a word = (a - d) - b * c``,