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/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

Source

val with_env : 
  (Environ.env -> Evd.evar_map -> Evd.evar_map * strategy) ->
  strategy

Sourceval matches : Pattern.constr_pattern -> strategy

Sourceval ltac1_tactic_call : unit Proofview.tactic -> strategy

Source

val tactic_call : 
  (env:Environ.env ->
    carrier:EConstr.constr ->
    lhs:EConstr.constr ->
    rel:EConstr.constr option ->
    Result.t Proofview.tactic) ->
  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