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 (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.engine/Evar_kinds/index.html

Module Evar_kindsSource

The kinds of existential variable

Should the obligation be defined (opaque or transparent (default)) or defined transparent and expanded in the term?

Sourcetype obligation_definition_status =
  1. | Define of bool
  2. | Expand
Sourcetype matching_var_kind =
  1. | FirstOrderPatVar of Names.Id.t
  2. | SecondOrderPatVar of Names.Id.t
Sourcetype subevar_kind =
  1. | Domain
  2. | Codomain
  3. | Body
Sourcetype record_field = {
  1. fieldname : Names.Constant.t;
  2. recordname : Names.inductive;
}
Sourcetype question_mark = {
  1. qm_obligation : obligation_definition_status;
  2. qm_name : Names.Name.t;
  3. qm_record_field : record_field option;
}
Sourceval default_question_mark : question_mark
Sourcetype t =
  1. | ImplicitArg of Names.GlobRef.t * int * Names.Id.t option * bool
    (*

    Force inference

    *)
  2. | BinderType of Names.Name.t
  3. | EvarType of Names.Id.t option * Evar.t
  4. | NamedHole of Names.Id.t
  5. | QuestionMark of question_mark
  6. | CasesType of bool
  7. | InternalHole
  8. | TomatchTypeParameter of Names.inductive * int
  9. | GoalEvar
  10. | ImpossibleCase
  11. | MatchingVar of matching_var_kind
  12. | VarInstance of Names.Id.t
  13. | SubEvar of subevar_kind option * Evar.t
Sourcetype glob_evar_kind =
  1. | GImplicitArg of Names.GlobRef.t * int * Names.Id.t option * bool
    (*

    Force inference

    *)
  2. | GBinderType of Names.Name.t
  3. | GNamedHole of bool * Names.Id.t
  4. | GQuestionMark of question_mark
  5. | GCasesType
  6. | GInternalHole
  7. | GImpossibleCase