		Search-engine friendly clone of the ACL2 documentation.

Std/basic

Lnfix

(lnfix x) is logically identical to (nfix x), but its guard requires that x is a natural number and, in the execution, it is just a no-op that returns x.

(lnfix x) is an inlined, enabled function that just expands into

(mbe :logic (nfix x) :exec x)

Why would you want this? When you defining a function whose guard assumes (natp n), it is often a good idea to write the function so that it logically treats non-naturals as 0. You might generally accomplish this by rewriting, e.g.,:

(defun my-function (n ...)
  (declare (xargs :guard (natp n)))
  <body>)

--->

(defun my-function (n ...)
  (declare (xargs :guard (natp n)))
  (let ((n (nfix n)))
    <body>))

This leads to a nice nat-equiv congruence rule. But since nfix has to check whether its argument is a natural number, and that has some performance cost.

By using lnfix in place of nfix here, you can get the same logical definition without this overhead.

Definitions and Theorems

Function: lnfix$inline

(defun lnfix$inline (x)
  (declare (xargs :guard (natp x)))
  (mbe :logic (nfix x) :exec x))