package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type (!'constr, !'types) pt =
  1. | LocalAssum of Names.Id.t binder_annot * 'types
  2. | LocalDef of Names.Id.t binder_annot * 'constr * 'types
val get_annot : ('a, 'b) pt -> Names.Id.t binder_annot
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 get_relevance : ('c, 't) pt -> Sorts.relevance
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 binder_annot * 'c option * 't
val of_tuple : (Names.Id.t binder_annot * 'c option * 't) -> ('c, 't) pt
val drop_body : ('c, 't) pt -> ('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
OCaml

Innovation. Community. Security.