package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

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

Sources

rocq-9.3.0.tar.gz

sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.tactics/Rewrite/index.html

Module `Rewrite`Source

TODO: document and clean me!

Sourceexception RewriteFailure of Environ.env * Evd.evar_map * Pretype_errors.pretype_error

Sourcetype evars = Evd.evar_map * Evar.Set.t

Sourcemodule Result : sig ... end

Sourcetype strategy

Source

val cl_rewrite_clause_strat : 
  strategy ->
  Names.Id.t option ->
  unit Proofview.tactic

Entry point for user-level "rewrite_strat"

Source

val cl_rewrite_clause : 
  EConstr.t Tactypes.with_bindings Tactypes.delayed_open ->
  bool ->
  Locus.occurrences ->
  Names.Id.t option ->
  unit Proofview.tactic

Entry point for user-level "setoid_rewrite"

Source

val is_applied_rewrite_relation : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_context ->
  EConstr.constr ->
  EConstr.types option

Source

val get_reflexive_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Source

val get_symmetric_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Source

val get_transitive_proof : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Sourceval setoid_symmetry : unit Proofview.tactic

Sourceval setoid_symmetry_in : Names.Id.t -> unit Proofview.tactic

Sourceval setoid_reflexivity : unit Proofview.tactic

Sourceval setoid_transitivity : EConstr.constr option -> unit Proofview.tactic

Sourcemodule Strategies : sig ... end

Sourcemodule Internal : sig ... end

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.tactics/Rewrite/index.html

Module RewriteSource

dune-project
Dependency

Module `Rewrite`Source