package coq

  1. Overview
  2. Docs
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 cst_member =
  1. | Cst_const of Constr.pconstant
  2. | Cst_proj of Names.Projection.t
type !'a member =
  1. | App of 'a app_node
  2. | Case of Constr.case_info * 'a * 'a array * Cst_stack.t
  3. | Proj of int * int * Names.Projection.t * Cst_stack.t
  4. | Fix of ('a, 'a) Constr.pfixpoint * 'a t * Cst_stack.t
  5. | Cst of cst_member * int * int list * 'a t * Cst_stack.t
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
val zip : ?refold:bool -> Evd.evar_map -> (EConstr.constr * EConstr.constr t) -> EConstr.constr
OCaml

Innovation. Community. Security.