IMAGPART

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

Completion Axiom (completion-of-imagpart): 

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

Guard for (imagpart x): 

(acl2-numberp x)