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 (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.tactics/Rewrite/index.html

Module RewriteSource

TODO: document and clean me!

Sourcetype unary_strategy =
  1. | Subterms
  2. | Subterm
  3. | Innermost
  4. | Outermost
  5. | Bottomup
  6. | Topdown
  7. | Progress
  8. | Try
  9. | Any
  10. | Repeat
Sourcetype binary_strategy =
  1. | Compose
Sourcetype nary_strategy =
  1. | Choice
Sourcetype ('constr, 'redexpr, 'id) strategy_ast =
  1. | StratId
  2. | StratFail
  3. | StratRefl
  4. | StratUnary of unary_strategy * ('constr, 'redexpr, 'id) strategy_ast
  5. | StratBinary of binary_strategy * ('constr, 'redexpr, 'id) strategy_ast * ('constr, 'redexpr, 'id) strategy_ast
  6. | StratNAry of nary_strategy * ('constr, 'redexpr, 'id) strategy_ast list
  7. | StratConstr of 'constr * bool
  8. | StratTerms of 'constr list
  9. | StratHints of bool * string
  10. | StratEval of 'redexpr
  11. | StratFold of 'constr
  12. | StratVar of 'id
  13. | StratFix of 'id * ('constr, 'redexpr, 'id) strategy_ast
Sourcetype rewrite_proof =
  1. | RewPrf of EConstr.constr * EConstr.constr
  2. | RewCast of Constr.cast_kind
Sourcetype rewrite_result_info = {
  1. rew_car : EConstr.constr;
  2. rew_from : EConstr.constr;
  3. rew_to : EConstr.constr;
  4. rew_prf : rewrite_proof;
  5. rew_evars : evars;
}
Sourcetype rewrite_result =
  1. | Fail
  2. | Identity
  3. | Success of rewrite_result_info
Sourcetype strategy
Sourceval map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('e -> 'f) -> ('a, 'c, 'e) strategy_ast -> ('b, 'd, 'f) strategy_ast
Sourceval pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> ('c -> Pp.t) -> ('a, 'b, 'c) strategy_ast -> Pp.t
Sourceval cl_rewrite_clause_strat : strategy -> Names.Id.t option -> unit Proofview.tactic

Entry point for user-level "rewrite_strat"

Entry point for user-level "setoid_rewrite"

Sourceval is_applied_rewrite_relation : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.constr -> EConstr.types option
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 Internal : sig ... end