1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
<html>
<head><title>NONNEGATIVE-INTEGER-QUOTIENT.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NONNEGATIVE-INTEGER-QUOTIENT</h2>natural number division function
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<pre>
Example Forms:
(nonnegative-integer-quotient 14 3) ; equals 4
(nonnegative-integer-quotient 15 3) ; equals 5
</pre>
<code>(nonnegative-integer-quotient i j)</code> returns the integer quotient
of the integers <code>i</code> and (non-zero) <code>j</code>, i.e., the largest <code>k</code>
such that <code>(* j k)</code> is less than or equal to <code>i</code>. Also
see <a href="FLOOR.html">floor</a>, see <a href="CEILING.html">ceiling</a> and see <a href="TRUNCATE.html">truncate</a>, which are
derived from this function and apply to rational numbers.
<p>
The <a href="GUARD.html">guard</a> of <code>(nonnegative-integer-quotient i j)</code> requires that
<code>i</code> is a nonnegative integer and <code>j</code> is a positive integer.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
