package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.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