Path extension

Keywords: path element

A path extension defines a successor path element separated from the preceding path by a dot (.).

Definition:

path_extension:= ext_op path_element