package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type struc_typ = {
  1. s_CONST : Names.constructor;
  2. s_EXPECTEDPARAM : int;
  3. s_PROJKIND : (Names.Name.t * bool) list;
  4. s_PROJ : Names.Constant.t option list;
}
type struc_tuple = Names.constructor * (Names.Name.t * bool) list * Names.Constant.t option list
val declare_structure : struc_tuple -> unit
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 declare_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 declare_canonical_structure : Names.GlobRef.t -> 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
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