Major Section: ACL2-BUILT-INS

Completion Axiom (completion-of-numerator):

completion-of-numerator

(equal (numerator x) (if (rationalp x) (numerator x) 0))

Guard for (numerator x):

(numerator x)

(rationalp x)