package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.interp/Constrintern/Interner/index.html

Module Constrintern.InternerSource

Sourcetype t = {
  1. ref : t -> (Libnames.qualid * Constrexpr.instance_expr option) fn;
  2. fix : t -> (Names.lident * Constrexpr.fix_expr list) fn;
  3. cofix : t -> (Names.lident * Constrexpr.cofix_expr list) fn;
  4. prodn : t -> (Constrexpr.local_binder_expr list * Constrexpr.constr_expr) fn;
  5. lambdan : t -> (Constrexpr.local_binder_expr list * Constrexpr.constr_expr) fn;
  6. letin : t -> (Names.lname * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr) fn;
  7. appexpl : t -> ((Libnames.qualid * Constrexpr.instance_expr option) * Constrexpr.constr_expr list) fn;
  8. app : t -> (Constrexpr.constr_expr * (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) list) fn;
  9. proj : t -> (Constrexpr.explicit_flag * (Libnames.qualid * Constrexpr.instance_expr option) * (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) list * Constrexpr.constr_expr) fn;
  10. record : t -> (Libnames.qualid * Constrexpr.constr_expr) list fn;
  11. cases : t -> (Constr.case_style * Constrexpr.constr_expr option * Constrexpr.case_expr list * Constrexpr.branch_expr list) fn;
  12. lettuple : t -> (Names.lname list * (Names.lname option * Constrexpr.constr_expr option) * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
  13. if_ : t -> (Constrexpr.constr_expr * (Names.lname option * Constrexpr.constr_expr option) * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
  14. hole : t -> Evar_kinds.glob_evar_kind option fn;
  15. genarg : t -> Genarg.raw_generic_argument fn;
  16. genargglob : t -> Genarg.glob_generic_argument fn;
  17. patvar : t -> Pattern.patvar fn;
  18. evar : t -> (Glob_term.existential_name CAst.t * (Names.lident * Constrexpr.constr_expr) list) fn;
  19. sort : t -> Constrexpr.sort_expr fn;
  20. cast : t -> (Constrexpr.constr_expr * Constr.cast_kind option * Constrexpr.constr_expr) fn;
  21. notation : t -> (Constrexpr.notation_with_optional_scope option * Constrexpr.notation * Constrexpr.constr_notation_substitution) fn;
  22. generalization : t -> (Glob_term.binding_kind * Constrexpr.constr_expr) fn;
  23. prim : t -> Constrexpr.prim_token fn;
  24. delimiters : t -> (Constrexpr.delimiter_depth * string * Constrexpr.constr_expr) fn;
  25. array : t -> (Constrexpr.instance_expr option * Constrexpr.constr_expr array * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
}