package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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