Module `Nameops.Name`

include module type of sig ... end

type t = Names.Name.t = | Anonymous | Name of Names.Id.t

val mk_name : Names.Id.t -> t
val is_anonymous : t -> bool
val is_name : t -> bool
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val hcons : t -> t
val print : t -> Pp.t

exception IsAnonymous

val fold_left : ('a -> Names.Id.t -> 'a) -> 'a -> Names.Name.t -> 'a: fold_left f na a is f id a if na is Name id, and a otherwise.

val fold_right : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a: fold_right f a na is f a id if na is Name id, and a otherwise.

val iter : (Names.Id.t -> unit) -> Names.Name.t -> unit: iter f na does f id if na equals Name id, nothing otherwise.

val map : (Names.Id.t -> Names.Id.t) -> Names.Name.t -> t: map f na is Anonymous if na is Anonymous and Name (f id) if na is Name id.

val fold_left_map : ('a -> Names.Id.t -> 'a * Names.Id.t) -> 'a -> Names.Name.t -> 'a * Names.Name.t: fold_left_map f a na is a',Name id' when na is Name id and f a id is (a',id'). It is a,Anonymous otherwise.

val fold_right_map : (Names.Id.t -> 'a -> Names.Id.t * 'a) -> Names.Name.t -> 'a -> Names.Name.t * 'a: fold_right_map f na a is Name id',a' when na is Name id and f id a is (id',a'). It is Anonymous,a otherwise.

val get_id : Names.Name.t -> Names.Id.t

get_id associates id to Name id.

raises IsAnonymous: otherwise.

val pick : Names.Name.t -> Names.Name.t -> Names.Name.t: pick na na' returns Anonymous if both names are Anonymous. Pick one of na or na' otherwise.

val pick_annot : Names.Name.t Context.binder_annot -> Names.Name.t Context.binder_annot -> Names.Name.t Context.binder_annot
val cons : Names.Name.t -> Names.Id.t list -> Names.Id.t list: cons na l returns id::l if na is Name id and l otherwise.

val to_option : Names.Name.t -> Names.Id.t option: to_option Anonymous is None and to_option (Name id) is Some id