package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

TODO: document and clean me!

exception RewriteFailure of Environ.env * Evd.evar_map * Pretype_errors.pretype_error
type unary_strategy =
  1. | Subterms
  2. | Subterm
  3. | Innermost
  4. | Outermost
  5. | Bottomup
  6. | Topdown
  7. | Progress
  8. | Try
  9. | Any
  10. | Repeat
type binary_strategy =
  1. | Compose
type nary_strategy =
  1. | Choice
type ('constr, 'redexpr) strategy_ast =
  1. | StratId
  2. | StratFail
  3. | StratRefl
  4. | StratUnary of unary_strategy * ('constr, 'redexpr) strategy_ast
  5. | StratBinary of binary_strategy * ('constr, 'redexpr) strategy_ast * ('constr, 'redexpr) strategy_ast
  6. | StratNAry of nary_strategy * ('constr, 'redexpr) 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
type rewrite_proof =
  1. | RewPrf of EConstr.constr * EConstr.constr
  2. | RewCast of Constr.cast_kind
type evars = Evd.evar_map * Evar.Set.t
type 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;
}
type rewrite_result =
  1. | Fail
  2. | Identity
  3. | Success of rewrite_result_info
type strategy
val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> ('a, 'b) strategy_ast -> Pp.t
val 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"

val is_applied_rewrite_relation : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.constr -> EConstr.types option
val setoid_symmetry : unit Proofview.tactic
val setoid_symmetry_in : Names.Id.t -> unit Proofview.tactic
val setoid_reflexivity : unit Proofview.tactic
val setoid_transitivity : EConstr.constr option -> unit Proofview.tactic
val apply_strategy : strategy -> Environ.env -> Names.Id.Set.t -> EConstr.constr -> (bool * EConstr.constr) -> evars -> rewrite_result
module Internal : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct