BITS_INTRO_CONV

wordsLib.BITS_INTRO_CONV : conv

Tries to convert terms of the form n MOD p, n MOD p DIV q and (n DIV q) MOD p into a terms of the form BITS h l n. This will succeed when p and q are powers of two.

Example

> wordsLib.BITS_INTRO_CONV “(n DIV 16) MOD 4”;
val it = ⊢ n DIV 16 MOD 4 = BITS 5 4 n: thm

> wordsLib.BITS_INTRO_CONV “n MOD 16 DIV 4”;
val it = ⊢ n MOD 16 DIV 4 = BITS 3 2 n: thm

> wordsLib.BITS_INTRO_CONV “n MOD 16”;
val it = ⊢ n MOD 16 = BITS 3 0 n: thm

> wordsLib.BITS_INTRO_CONV “n MOD dimword(:'a)”;
val it = ⊢ n MOD dimword (:α) = BITS (dimindex (:α) − 1) 0 n: thm

See also

wordsLib.BITS_INTRO_ss