package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type proj_kind = {
  1. pk_name : Names.Name.t;
  2. pk_true_proj : bool;
  3. pk_canonical : bool;
}
type struc_typ = {
  1. s_CONST : Names.constructor;
  2. s_EXPECTEDPARAM : int;
  3. s_PROJKIND : proj_kind list;
  4. s_PROJ : Names.Constant.t option list;
}
type struc_tuple = Names.constructor * proj_kind list * Names.Constant.t option list
val register_structure : Environ.env -> struc_tuple -> unit
val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
val lookup_structure : Names.inductive -> struc_typ
val lookup_projections : Names.inductive -> Names.Constant.t option list
val find_projection_nparams : Names.GlobRef.t -> int
val find_projection : Names.GlobRef.t -> struc_typ
val is_projection : Names.Constant.t -> bool
val register_primitive_projection : Names.Projection.Repr.t -> Names.Constant.t -> unit
val is_primitive_projection : Names.Constant.t -> bool
val find_primitive_projection : Names.Constant.t -> Names.Projection.Repr.t option
type cs_pattern =
  1. | Const_cs of Names.GlobRef.t
  2. | Prod_cs
  3. | Sort_cs of Sorts.family
  4. | Default_cs
type obj_typ = {
  1. o_DEF : Constr.constr;
  2. o_CTX : Univ.AUContext.t;
  3. o_INJ : int option;
  4. o_TABS : Constr.constr list;
  5. o_TPARAMS : Constr.constr list;
  6. o_NPARAMS : int;
  7. o_TCOMPS : Constr.constr list;
}
val cs_pattern_of_constr : Environ.env -> Constr.constr -> cs_pattern * int option * Constr.constr list
val pr_cs_pattern : cs_pattern -> Pp.t
val lookup_canonical_conversion : (Names.GlobRef.t * cs_pattern) -> Constr.constr * obj_typ
val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> (Names.Constant.t * Names.inductive) -> unit
val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool
val canonical_projections : unit -> ((Names.GlobRef.t * cs_pattern) * obj_typ) list
val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Names.Constant.t * Names.inductive
OCaml

Innovation. Community. Security.