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