package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val mkNamedProd_or_LetIn : Constr.named_declaration -> Constr.types -> Constr.types
val mkNamedProd_wo_LetIn : Constr.named_declaration -> Constr.types -> Constr.types
val mkLambda_or_LetIn : Constr.rel_declaration -> Constr.constr -> Constr.constr
val mkNamedLambda_or_LetIn : Constr.named_declaration -> Constr.constr -> Constr.constr
val applist : (Constr.constr * Constr.constr list) -> Constr.constr
val applistc : Constr.constr -> Constr.constr list -> Constr.constr
val appvect : (Constr.constr * Constr.constr array) -> Constr.constr
val appvectc : Constr.constr -> Constr.constr array -> Constr.constr
val to_lambda : int -> Constr.constr -> Constr.constr
val to_prod : int -> Constr.constr -> Constr.constr
val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
val it_mkProd_or_LetIn : Constr.types -> Constr.rel_context -> Constr.types
val lambda_applist : Constr.constr -> Constr.constr list -> Constr.constr
val lambda_appvect : Constr.constr -> Constr.constr array -> Constr.constr
val lambda_applist_assum : int -> Constr.constr -> Constr.constr list -> Constr.constr
val lambda_appvect_assum : int -> Constr.constr -> Constr.constr array -> Constr.constr
val prod_appvect : Constr.types -> Constr.constr array -> Constr.types
val prod_applist : Constr.types -> Constr.constr list -> Constr.types
val prod_appvect_assum : int -> Constr.types -> Constr.constr array -> Constr.types
val prod_applist_assum : int -> Constr.types -> Constr.constr list -> Constr.types
val decompose_prod_n : int -> Constr.constr -> (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr
val decompose_prod_assum : Constr.types -> Constr.rel_context * Constr.types
val decompose_lam_assum : Constr.constr -> Constr.rel_context * Constr.constr
val decompose_prod_n_assum : int -> Constr.types -> Constr.rel_context * Constr.types
val decompose_lam_n_assum : int -> Constr.constr -> Constr.rel_context * Constr.constr
val decompose_lam_n_decls : int -> Constr.constr -> Constr.rel_context * Constr.constr
val prod_assum : Constr.types -> Constr.rel_context
val prod_n_assum : int -> Constr.types -> Constr.rel_context
val lam_n_assum : int -> Constr.constr -> Constr.rel_context
val strip_prod : Constr.types -> Constr.types
val strip_lam : Constr.constr -> Constr.constr
val strip_prod_n : int -> Constr.types -> Constr.types
val strip_lam_n : int -> Constr.constr -> Constr.constr
val strip_prod_assum : Constr.types -> Constr.types
val strip_lam_assum : Constr.constr -> Constr.constr
val mkArity : arity -> Constr.types
val destArity : Constr.types -> arity
val isArity : Constr.types -> bool
type sorts_family = Sorts.family =
  1. | InSProp
  2. | InProp
  3. | InSet
  4. | InType
  • deprecated Alias for Sorts.family
type sorts = private Sorts.t =
  1. | SProp
  2. | Prop
  3. | Set
  4. | Type of Univ.Universe.t
  • deprecated Alias for Sorts.t