package coq

  1. Overview
  2. Docs
package coq
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.

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