package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Declaration : sig ... end
type (!'constr, !'types) pt = ('constr, 'types) Declaration.pt list
val empty : ('c, 't) pt
val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
val length : ('c, 't) pt -> int
val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
val nhyps : ('c, 't) pt -> int
val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt
val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
val iter : ('c -> unit) -> ('c, 'c) pt -> unit
val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a
val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
val to_tags : ('c, 't) pt -> bool list
val drop_bodies : ('c, 't) pt -> ('c, 't) pt
val to_extended_list : (int -> 'r) -> int -> ('c, 't) pt -> 'r list
val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array