Filtering...

realfix

books/std/basic/realfix

Included Books

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