		Search-engine friendly clone of the ACL2 documentation.

Reference-types-definition

Reference-type

Fixtype of Java (unannotated) reference types [JLS14:4.3] [JLS14:8.3].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:class → reference-type-class
:array → reference-type-array
:variable → reference-type-variable

This corresponds to the grammar rule for unann-reference-type.

As explained in class-type, our class-type fixtype corresponds to unann-class-or-interface-type, unann-class-type, and unann-interface-type in the grammar.

An (unannotated) type variable is a type identifier, according to the rule for unann-type-variable.

Subtopics

Reference-type-case: Case macro for the different kinds of reference-type structures.
Reference-type-equiv: Basic equivalence relation for reference-type structures.
Reference-type-variable
Reference-type-class
Reference-type-array
Reference-typep: Recognizer for reference-type structures.
Reference-type-kind: Get the kind (tag) of a reference-type structure.
Reference-type-fix: Fixing function for reference-type structures.
Reference-type-count: Measure for recurring over reference-type structures.