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 lookup : Names.Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt
val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
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_vars : ('c, 't) pt -> Names.Id.Set.t
val drop_bodies : ('c, 't) pt -> ('c, 't) pt
val to_instance : (Names.Id.t -> 'r) -> ('c, 't) pt -> 'r list