package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type rewrite_attributes
val rewrite_attributes : rewrite_attributes Attributes.attribute
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
  2. | 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. | StratConstr of 'constr * bool
  7. | StratTerms of 'constr list
  8. | StratHints of bool * string
  9. | StratEval of 'redexpr
  10. | 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
val is_applied_rewrite_relation : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.constr -> EConstr.types option
val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t option
val default_morphism : ((EConstr.types * EConstr.constr option) option list * (EConstr.types * EConstr.types option) option) -> EConstr.constr -> EConstr.constr * EConstr.constr
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
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