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 option list;
}
type struc_tuple = Names.inductive * Names.constructor * (Names.Name.t * bool) list * Names.constant option list
val declare_structure : struc_tuple -> unit
val lookup_structure : Names.inductive -> struc_typ
val lookup_projections : Names.inductive -> Names.constant option list
val find_projection_nparams : Globnames.global_reference -> int
val find_projection : Globnames.global_reference -> struc_typ
type cs_pattern =
  1. | Const_cs of Globnames.global_reference
  2. | Prod_cs
  3. | Sort_cs of Term.sorts_family
  4. | Default_cs
type obj_typ = {
  1. o_DEF : Term.constr;
  2. o_CTX : Univ.ContextSet.t;
  3. o_INJ : int option;
  4. o_TABS : Term.constr list;
  5. o_TPARAMS : Term.constr list;
  6. o_NPARAMS : int;
  7. o_TCOMPS : Term.constr list;
}
val cs_pattern_of_constr : Environ.env -> Term.constr -> cs_pattern * int option * Term.constr list
val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
val lookup_canonical_conversion : (Globnames.global_reference * cs_pattern) -> Term.constr * obj_typ
val declare_canonical_structure : Globnames.global_reference -> unit
val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool
val canonical_projections : unit -> ((Globnames.global_reference * 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