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

Authors

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

Maintainers

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

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

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

Module AutoSource

This files implements auto and related automation tactics

Sourceval compute_secvars : Proofview.Goal.t -> Names.Id.Pred.t
Sourceval get_reference_hints : Environ.env -> Evd.evar_map -> Tactypes.delayed_open_constr list -> Names.GlobRef.t list
Sourceval default_search_depth : int

Default maximum search depth used by auto and trivial.

Try unification with the precompiled clause, then use registered Apply

ConclPattern concl pat tacast: if the term concl matches the pattern pat, (in sense of Pattern.somatches, then replace ?1 ?2 metavars in tacast by the right values to build a tactic

Sourceval default_auto : unit Proofview.tactic

default_auto runs the tactic auto with:

  • Maximum search depth default_search_depth.
  • The hint database "core".
  • No additional lemma.
Sourceval gen_auto : ?debug:Hints.debug -> int option -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic

gen_auto ?debug depth lemmas hints runs the tactic auto.

  • debug controls whether to print a debug trace (Off by default). Off prints nothing, Info prints successful steps, and Debug prints all steps (including unsuccessful ones).
  • depth is the maximum search depth. If None, default_search_depth is used.
  • lemmas contains additional lemmas for auto to use.
  • hints is a list of hint databases to use. If None, _all_ existing hint databases are used. By default the "core" hint database is included: passing "nocore" will disable "core".
Sourceval gen_trivial : ?debug:Hints.debug -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic

gen_trivial runs the tactic trivial. See gen_auto for an explanation of the different options.