		Search-engine friendly clone of the ACL2 documentation.

Arith-compare-check

My-trunc

Signature
(my-trunc x y) → *
Arguments: x — Guard (integerp x).; y — Guard (integerp y).

Definitions and Theorems

Function: my-trunc

(defun my-trunc (x y)
  (declare (xargs :guard (and (integerp x) (integerp y))))
  (let ((__function__ 'my-trunc))
    (declare (ignorable __function__))
    (mbe :logic (truncate x y)
         :exec (if (eql y 0) 0 (truncate x y)))))