1\DOC
2
3\TYPE {SIZES_ss : ssfrag}
4
5\SYNOPSIS
6
7Simplification fragment for words.
8
9\KEYWORDS
10
11simplification, words.
12
13\DESCRIBE
14
15The fragment {SIZES_ss} evaluates terms {``dimindex(:'a)``}, {``dimword(:'a)``},
16{``INT_MIN(:'a)``}, and {``FINITE (UNIV : 'a set)``} for numeric types.
17
18\EXAMPLE
19{
20- SIMP_CONV (pure_ss++SIZES_ss) [] ``dimindex(:32) + INT_MIN(:32) + dimword(:32)``
21> val it =
22    |- dimindex (:32) + INT_MIN (:32) + dimword (:32) =
23       32 + 2147483648 + 4294967296 : thm
24}
25
26\SEEALSO
27
28wordsLib.SIZES_CONV, wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss,
29wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_SHIFT_ss,
30wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss,
31wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss
32
33\ENDDOC
34