package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type (!'constr, !'types) pt =

type t = (Constr.constr, Constr.types) pt

val get_id : ('c, 't) pt -> Names.Id.t

val get_value : ('c, 't) pt -> 'c option

val get_type : ('c, 't) pt -> 't

val set_id : Names.Id.t -> ('c, 't) pt -> ('c, 't) pt

val set_type : 't -> ('c, 't) pt -> ('c, 't) pt

val is_local_assum : ('c, 't) pt -> bool

val is_local_def : ('c, 't) pt -> bool

val exists : ('c -> bool) -> ('c, 'c) pt -> bool

val for_all : ('c -> bool) -> ('c, 'c) pt -> bool

val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

val map_id : (Names.Id.t -> Names.Id.t) -> ('c, 't) pt -> ('c, 't) pt

val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt

val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt

val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit

val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a

val to_tuple : ('c, 't) pt -> Names.Id.t * 'c option * 't

val of_tuple : (Names.Id.t * 'c option * 't) -> ('c, 't) pt

val of_rel_decl : 
  (Names.Name.t -> Names.Id.t) ->
  ('c, 't) Rel.Declaration.pt ->
  ('c, 't) pt

val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt