		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))
  (make-ienv :version (c::version-c17)
             :short-bytes 2
             :int-bytes 2
             :long-bytes 4
             :llong-bytes 8
             :plain-char-signedp nil))