REALPART

real part of a complex number
Major Section:  ACL2-BUILT-INS

Completion Axiom (completion-of-realpart):

(equal (realpart x)
       (if (acl2-numberp x)
           (realpart x)
         0))

Guard for (realpart x):

(acl2-numberp x)