----------------------------------------------------------------------
n2w_INTRO_TAC                                               (wordsLib)
----------------------------------------------------------------------
n2w_INTRO_TAC : int -> tactic

DESCRIBE
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
blastLib.BBLAST_CONV.

----------------------------------------------------------------------