Constructors
Members
A type for names of the same kind as this name
A type for names of the same kind as this name
This name converted to a term name
This name converted to a term name
This name downcasted to a term name
This name downcasted to a term name
This name downcasted to a type name
This name downcasted to a type name
Replace $op_name's by corresponding operator symbols.
Replace $op_name's by corresponding operator symbols.
Replace operator symbols by corresponding $op_name's.
Replace operator symbols by corresponding $op_name's.
Is this name a term name?
Is this name a term name?
Is this name a type name?
Is this name a type name?
A name in the same (term or type) namespace as this name and
with same characters as given name
.
A name in the same (term or type) namespace as this name and
with same characters as given name
.
This name converted to a type name
This name converted to a type name