package coq-core
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
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