SIZES_ss : ssfrag
STRUCTURE
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
HOL  Kananaskis-13