package coq

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

This files implements the autorewrite tactic.

Rewriting rules before tactic interpretation

val add_rew_rules : locality:Goptions.option_locality -> string -> raw_rew_rule list -> unit

To add rewriting rules to a base

val autorewrite : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> unit Proofview.tactic

The AutoRewrite tactic. The optional conditions tell rewrite how to handle matching and side-condition solving. Default is Naive: first match in the clause, don't look at the side-conditions to tell if the rewrite succeeded.

val autorewrite_in : ?conds:Equality.conditions -> Names.Id.t -> unit Proofview.tactic -> string list -> unit Proofview.tactic
type rew_rule = {
  1. rew_lemma : Constr.constr;
  2. rew_type : Constr.types;
  3. rew_pat : Constr.constr;
  4. rew_ctx : Univ.ContextSet.t;
  5. rew_l2r : bool;
  6. rew_tac : Genarg.glob_generic_argument option;
}

Rewriting rules

val find_rewrites : string -> rew_rule list
val find_matches : string -> Constr.constr -> rew_rule list
val auto_multi_rewrite : ?conds:Equality.conditions -> string list -> Locus.clause -> unit Proofview.tactic
val auto_multi_rewrite_with : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
val print_rewrite_hintdb : string -> Pp.t
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