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

Definitions and Theorems

Function: ienv-default

(defun ienv-default nil
  (declare (xargs :guard t))
  (let ((__function__ 'ienv-default))
    (declare (ignorable __function__))
    (make-ienv :short-bytes 2
               :int-bytes 4
               :long-bytes 8
               :llong-bytes 8
               :plain-char-signedp nil)))