package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

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 =
  1. | Anonymous
    (*

    anonymous identifier

    *)
  2. | Name of Names.Id.t
    (*

    non-anonymous identifier

    *)
val mk_name : Names.Id.t -> t

constructor

val is_anonymous : t -> bool

Return true iff a given name is Anonymous.

val is_name : t -> bool

Return true iff a given name is Name _.

val compare : t -> t -> int

Comparison over names.

val equal : t -> t -> bool

Equality over names.

val hash : t -> int

Hash over names.

val hcons : t -> t

Hashconsing over names.

val print : t -> Pp.t

Pretty-printer (print "_" for Anonymous.

Sourceexception IsAnonymous
Sourceval 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.

Sourceval 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.

Sourceval iter : (Names.Id.t -> unit) -> Names.Name.t -> unit

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.

Sourceval 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.

Sourceval 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.

get_id associates id to Name id.

pick na na' returns Anonymous if both names are Anonymous. Pick one of na or na' otherwise.

Sourceval 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.

Sourceval to_option : Names.Name.t -> Names.Id.t option

to_option Anonymous is None and to_option (Name id) is Some id