Lines Matching refs:word
67 STM1 f (b: word32) (registers: 'a word) s m j =
80 STM_UPTO f i (registers: 'a word) (b: word32, s) =
203 \\ Cases_on `word_msb (x + y) <> word_msb (1w : 'a word)`
339 `!registers: 'a word.
346 `!r: 'a word.
460 (((31 >< 1) r : 31 word @@ (0w: word1)) = r)`,
467 (((31 >< 1) (w + 4w) : 31 word @@ (1w: word1)) = (w + 4w) !! 1w)`,
474 (((31 >< 1) (w + 4w - 2w) : 31 word @@ (1w: word1)) = (w + 2w) !! 1w)`,
488 `aligned 1 (w: 31 word @@ (0w: word1))`,
760 ((w2w w : 33 word) << imm) ' 32 = testbit 32 (shiftl (w2v w) imm)`,
771 ((w << imm2, if imm2 = 0 then C else ((w2w w : 33 word) << imm2) ' 32),
786 else (w << amount, ((w2w w : 33 word) << amount) ' 32)
823 if amount = 0 then C else ((w2w w : 33 word) << amount) ' 32)
974 `!n f registers:'a word b s.