package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/coq-core.engine/Nameops/Name/index.html
Module Nameops.NameSource
include module type of struct include Names.Name end
type t = Names.Name.t = | Anonymous(*anonymous identifier
*)| Name of Names.Id.t(*non-anonymous identifier
*)
val mk_name : Names.Id.t -> tconstructor
val is_anonymous : t -> boolReturn true iff a given name is Anonymous.
val is_name : t -> boolReturn true iff a given name is Name _.
val hash : t -> intHash over names.
fold_left f na a is f id a if na is Name id, and a otherwise.
fold_right f a na is f a id if na is Name id, and a otherwise.
iter f na does f id if na equals Name id, nothing otherwise.
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.tfold_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 * 'afold_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.
get_id associates id to Name id.
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_annotcons na l returns id::l if na is Name id and l otherwise.
to_option Anonymous is None and to_option (Name id) is Some id