Macro to introduce an abstract placeholder for a unary operation or a conversion involving floating-point values.
Macro:
(defmacro def-primitive-unary-abs (name type) (cons 'make-event (cons (cons 'def-primitive-unary-abs-fn (cons (cons 'quote (cons name 'nil)) (cons type 'nil))) 'nil)))
Function:
(defun def-primitive-unary-abs-fn (name type) (declare (xargs :guard (and (symbolp name) (primitive-typep type)))) (let ((__function__ 'def-primitive-unary-abs-fn)) (declare (ignorable __function__)) (b* ((result (def-primitive-unary/binary-abs-term type)) (predicate (def-primitive-unary/binary-abs-predicate type)) (thm-name (add-suffix name "-TYPE"))) (cons 'encapsulate (cons (cons (cons (cons name '(*)) '(=> *)) 'nil) (cons (cons 'local (cons (cons 'defun (cons name (cons '(x) (cons '(declare (ignore x)) (cons result 'nil))))) 'nil)) (cons (cons 'defthm (cons thm-name (cons (cons predicate (cons (cons name '(x)) 'nil)) 'nil))) 'nil)))))))