DEFABBREV : THE Type declarations are needed for compile time efficiency Inline declarations performed using THE forms Macros can be used to "wrap" THE forms around terms (defmacro Int32 (x) `(the (signed-byte 32) ,x)) THE forms don't work well with deep LET bindings Defeats ACL2 heuristics Introduces unecessary case splits Inhibits beta reduction THE forms ultimately interfere with proofs See Demonstration