		Search-engine friendly clone of the ACL2 documentation.

Shape-specs

G-int

Create a g-binding for an integer.

This is a low-level way to create a custom shape specifier for a signed integer. You might generally prefer higher-level tools like auto-bindings.

Definitions and Theorems

Function: g-int

(defun g-int (start by n)
  (declare (xargs :guard (and (acl2-numberp start)
                              (acl2-numberp by)
                              (natp n))))
  (g-integer (numlist start by n)))