ref Production

Definition

ref : ref . identifier
    | identifier

Purpose

A ref is used to resolve a reference to a particular element in a module, or to an element in the current context. It is similar to a field_exp.

Semantics

In the first production, the ref must refer to a module. identifier must refer to a signature.