Quelle autorewrite.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** This files implements the autorewrite tactic. *)

open Constr
open Equality

type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Gentactic.raw_generic_tactic option) CAst.t

(** To add rewriting rules to a base *)
val add_rew_rules : locality:Hints.hint_locality -> string -> raw_rew_rule list -> unit

val add_rewrite_hint
  : locality:Libobject.locality
  -> poly:bool
  -> string list
  -> bool
  -> Gentactic.raw_generic_tactic option -> Constrexpr.constr_expr list -> unit

(** 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 : ?conds:conditions -> unit Proofview.tactic -> string list -> unit Proofview.tactic
val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic -> string list -> unit Proofview.tactic

(** Rewriting rules *)
module RewRule :
sig
   type t
   val rew_lemma : t -> Univ.ContextSet.t * constr
   val rew_l2r : t -> bool
   val rew_tac : t -> Gentactic.glob_generic_tactic option
end

val find_rewrites : string -> RewRule.t list

val find_matches : Environ.env -> string -> constr -> RewRule.t list

val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> unit Proofview.tactic

val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic

val print_rewrite_hintdb : string -> Pp.t

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.