[Hol-info] convert an SML int variable into a word32 term?

Hey, Suppose there is a variable in SML: val v = 0xA How can I get a term which has the value of "v" in word32? I found mk_word in wordsSyntax, but I have no idea what the second parameter should be (I guess the first might be v)? Thanks. Lu --

Re: [Hol-info] convert an SML int variable into a word32 term?

The second parameter is the word length. For example: wordsSyntax.mk_word (Arbnum.fromInt 0xA, Arbnum.fromInt 32) For convenience, there is also wordsSyntax.mk_wordi (Arbnum.fromInt 0xA, 32) and wordsSyntax.mk_wordii (0xA, 32) Be aware that Mosml integers are 31 bits wide. For example: - m