n2w_INTRO_TAC : int -> tactic
STRUCTURE
wordsLib
DESCRIPTION
The tactic n2w_INTRO_TAC i attempts to recast finite problems (over num) of the form m = n, m < n and m <= n into problems over bit-vectors of size i.
EXAMPLE
Given the goal: 
?- w2n (a: word4) + w2n (b: word4) < 32
applying 
e (wordsLib.n2w_INTRO_TAC 6)
gives the new goal 
[ w2n a < 16, w2n b < 16 ] ?- w2w a + w2w b <+ 32w
This goal can be solved using blastLib.BBLAST_TAC. Any word length strictly greater than five would have sufficed here; it is generally best to pick as small a word size as is necessary.
SEEALSO
BBLAST_CONV
HOL  Kananaskis-14