package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
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, 'r) Context.pbinder_annot ->
(Names.Name.t, 'r) Context.pbinder_annot ->
(Names.Name.t, 'r) Context.pbinder_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