Names.Constant
type t
Constructors
val make : KerName.t -> KerName.t -> t
Builds a constant name from a user and a canonical kernel name.
val make1 : KerName.t -> t
Special case of make where the user name is canonical.
make
val make2 : ModPath.t -> Id.t -> t
Shortcut for (make1 (KerName.make ...))
(make1 (KerName.make ...))
Projections
val user : t -> KerName.t
val canonical : t -> KerName.t
val modpath : t -> ModPath.t
Shortcut for KerName.modpath (user ...)
KerName.modpath (user ...)
val label : t -> Id.t
Shortcut for KerName.label (user ...)
KerName.label (user ...)
Comparisons
include QNameS with type t := t
module CanOrd : EqType with type t = t
Equality functions over the canonical name. Their use should be restricted to the kernel.
module UserOrd : EqType with type t = t
Equality functions over the user name.
val canonize : t -> t
Returns the canonical version of the name
val change_label : t -> Id.t -> t
Builds a new constant name with a different label
Displaying
val to_string : t -> string
Encode as a string (not to be used for user-facing messages).
val print : t -> Pp.t
Print internal representation (not to be used for user-facing messages).
val debug_to_string : t -> string
Same as to_string, but outputs extra information related to debug.
to_string
val debug_print : t -> Pp.t
Same as print, but outputs extra information related to debug.
print