package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type (!'constr, !'types) pt =
  1. | LocalAssum of Names.Name.t binder_annot * 'types
  2. | LocalDef of Names.Name.t binder_annot * 'constr * 'types
val get_annot : ('a, 'b) pt -> Names.Name.t binder_annot
val get_name : ('c, 't) pt -> Names.Name.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_name : Names.Name.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_name : (Names.Name.t -> Names.Name.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 map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) 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.Name.t binder_annot * 'c option * 't
val drop_body : ('c, 't) pt -> ('c, 't) pt