package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a app_node
val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
type !'a member =
  1. | App of 'a app_node
  2. | Case of Constr.case_info * 'a * ('a, EConstr.EInstance.t) Constr.case_invert * 'a array
  3. | Proj of Names.Projection.t
  4. | Fix of ('a, 'a) Constr.pfixpoint * 'a t
  5. | Primitive of CPrimitives.t * Names.Constant.t * EConstr.EInstance.t * 'a t * CPrimitives.args_red
and !'a t = 'a member list
val pr : ('a -> Pp.t) -> 'a t -> Pp.t
val empty : 'a t
val is_empty : 'a t -> bool
val append_app : 'a array -> 'a t -> 'a t
val decomp : 'a t -> ('a * 'a t) option
val decomp_node_last : 'a app_node -> 'a t -> 'a * 'a t
val compare_shape : 'a t -> 'a t -> bool
exception IncompatibleFold2
val fold2 : ('a -> EConstr.constr -> EConstr.constr -> 'a) -> 'a -> EConstr.constr t -> EConstr.constr t -> 'a
val map : ('a -> 'a) -> 'a t -> 'a t
val append_app_list : 'a list -> 'a t -> 'a t
val strip_app : 'a t -> 'a t * 'a t
val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
val not_purely_applicative : 'a t -> bool
val list_of_app_stack : EConstr.constr t -> EConstr.constr list option
val assign : 'a t -> int -> 'a -> 'a t
val args_size : 'a t -> int
val tail : int -> 'a t -> 'a t
val nth : 'a t -> int -> 'a