(in-package "ACL2")
(include-book "xdoc/constructors" :dir :system)
(defsection std/basic/ifix :parents (std/basic ifix) :short "Rules about @(tsee ifix)." (defthm ifix-when-integerp (implies (integerp x) (equal (ifix x) x))) (defthmd integerp-of-ifix (integerp (ifix x))))