		Search-engine friendly clone of the ACL2 documentation.

Definterface-hash-infop

Information about a definterface-hash interface, recorded as a pair's value in the definterface-hash table.

(definterface-hash-infop x) is a std::defaggregate of the following fields.

input-size-limit — The :input-size-limit input.
Invariant (maybe-posp input-size-limit).
output-size — The :output-size input.
Invariant (posp output-size).

Source link: definterface-hash-infop

The name of the interface is the key of the pair in the table.

Make-definterface-hash-info: Constructor macro for definterface-hash-infop structures.
Definterface-hash-info: Raw constructor for definterface-hash-infop structures.
Change-definterface-hash-info: A copying macro that lets you create new definterface-hash-infop structures, based on existing structures.
Make-honsed-definterface-hash-info: Constructor macro for honsed definterface-hash-infop structures.
Honsed-definterface-hash-info: Raw constructor for honsed definterface-hash-infop structures.
Definterface-hash-info->output-size: Access the output-size field of a definterface-hash-infop structure.
Definterface-hash-info->input-size-limit: Access the input-size-limit field of a definterface-hash-infop structure.