<names> ::= <name-primary>+, | <name-primary> ("/" <name-primary>)+ | <name-primary> ("~" <name-primary>)+ <name-primary> ::= <name-pattern> | <class> | "(" [ <names> ] ")" <name-pattern> ::= <prefix-pattern> [ . ] | <prefix-pattern> <extension>+ [ : <last> ] [ ! ] <prefix-pattern> ::= ( <simpleId> | "*" )+ <last> ::= <number> | last
arith, set.2:last *Hyp * ~ (nat, set)
Primitive <names> include <name>s (e.g., set.2) and <name-pattern>s of the following forms, where N is a <name> that may have asterisks embedded in its alphanumeric prefix (e.g., * and *Hyp.1), and where m and n are positive integers.
Pattern Facts denoted by pattern ------- ------------------------ N! those with names that can be obtained from N by replacing the asterisks in N by alphanumeric characters N those denoted by N! and all their descendents N.m:n! those denoted by N.m!, N.m+1!, ..., N.n! N.m:n those denoted by N.m, N.m+1, ..., N.n N.m:last! those denoted N.m!, N.m+1!, ... N.m:last those denoted N.m, N.m+1, ...
See also <class>.