package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. Refiner errors.
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.proofs/Logic/index.html

Module LogicSource

Legacy proof engine. Do not use in newly written code.

check respectively means:\\ Intro: check that the name does not exist\\ Intro_after: check that the name does not exist and that variables in its type does not escape their scope\\ Intro_replacing: check that the name does not exist and that variables in its type does not escape their scope\\ Convert_hyp: check that the name exist and that its type is convertible\\

Refiner errors.
Sourcetype refiner_error =
  1. | UnresolvedBindings of Names.Name.t list
  2. | CannotApply of EConstr.t * EConstr.t
  3. | NonLinearProof of EConstr.t
  4. | IntroNeedsProduct
  5. | NoSuchHyp of Names.Id.t
Sourceexception RefinerError of Environ.env * Evd.evar_map * refiner_error
Sourceval error_no_such_hypothesis : Environ.env -> Evd.evar_map -> Names.Id.t -> 'a

Move destination for hypothesis

Sourcetype 'id move_location =
  1. | MoveAfter of 'id
  2. | MoveBefore of 'id
  3. | MoveFirst
  4. | MoveLast
    (*

    can be seen as "no move" when doing intro

    *)
Sourceval pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t
Sourceval convert_hyp : check:bool -> reorder:bool -> Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Environ.named_context_val
Sourcetype cannot_move_hyp
Sourceexception CannotMoveHyp of cannot_move_hyp