		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Ienv-default

A default implementation environment.

Signature
(ienv-default) → *

This has no particular significance, but we set all the byte sizes to their minima, and the plain char flag to nil (i.e. unsigned); we also disable GCC extensions.

Definitions and Theorems

Function: ienv-default

(defun ienv-default nil
  (declare (xargs :guard t))
  (let ((__function__ 'ienv-default))
    (declare (ignorable __function__))
    (ienv-simple 2 2 4 8 nil nil)))