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 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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct