n2w_INTRO_TAC : int -> tactic

- STRUCTURE
- 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:applying
?- w2n (a: word4) + w2n (b: word4) < 32

gives the new goale (wordsLib.n2w_INTRO_TAC 6)

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.[ w2n a < 16, w2n b < 16 ] ?- w2w a + w2w b <+ 32w

- SEEALSO

HOL Kananaskis-14