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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

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

Sources

rocq-9.2.0.tar.gz

sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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

Module `Rewrite.Strategies`Source

Sourceval fail : strategy

Sourceval id : strategy

Sourceval refl : strategy

Sourceval progress : strategy -> strategy

Sourceval seq : strategy -> strategy -> strategy

Sourceval seqs : strategy list -> strategy

Sourceval choice : strategy -> strategy -> strategy

Sourceval choices : strategy list -> strategy

Sourceval try_ : strategy -> strategy

Source

val fix_tac : 
  (strategy -> strategy Proofview.tactic) ->
  strategy Proofview.tactic

Sourceval fix : (strategy -> strategy) -> strategy

Sourceval any : strategy -> strategy

Sourceval repeat : strategy -> strategy

Sourceval all_subterms : strategy -> strategy

Sourceval one_subterm : strategy -> strategy

Sourceval bottomup : strategy -> strategy

Sourceval topdown : strategy -> strategy

Sourceval innermost : strategy -> strategy

Sourceval outermost : strategy -> strategy

Source

val one_lemma : 
  Tactypes.delayed_open_constr ->
  bool ->
  Gentactic.glob_generic_tactic option ->
  Locus.occurrences ->
  strategy

Source

val lemmas : 
  (Tactypes.delayed_open_constr * bool * Gentactic.glob_generic_tactic option)
    list ->
  strategy

Sourceval old_hints : string -> strategy

Sourceval hints : string -> strategy

Sourceval reduce : Redexpr.red_expr -> strategy

Sourceval fold : Evd.econstr -> strategy

Sourceval fold_glob : Glob_term.glob_constr -> strategy

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

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

Module Rewrite.StrategiesSource

dune-project
Dependency

Module `Rewrite.Strategies`Source