SIZES_ss : ssfrag
STRUCTURE
wordsLib
SYNOPSIS
Simplification fragment for words.
DESCRIPTION
The fragment SIZES_ss evaluates terms ``dimindex(:'a)``, ``dimword(:'a)``, ``INT_MIN(:'a)``, and ``FINITE (UNIV : 'a set)`` for numeric types.
EXAMPLE
- SIMP_CONV (pure_ss++SIZES_ss) [] ``dimindex(:32) + INT_MIN(:32) + dimword(:32)``
> val it =
    |- dimindex (:32) + INT_MIN (:32) + dimword (:32) =
       32 + 2147483648 + 4294967296 : thm
SEEALSO
SIZES_CONV, WORD_CONV, FCP_ss, BIT_ss, WORD_ARITH_ss, WORD_LOGIC_ss, WORD_SHIFT_ss, WORD_ARITH_EQ_ss, WORD_BIT_EQ_ss, WORD_EXTRACT_ss, WORD_MUL_LSL_ss, WORD_ss
HOL  Kananaskis-13