# 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))