|
(* An example of unification in rewrite which uses eager substitution
of metas (provided by Pierre-Marie).
Put in the test suite as an indication of what the use metas
eagerly flag provides, even though the concrete cases that use it
are seldom. Today supported thanks to a new flag for using evars
eagerly, after this variant of setoid rewrite started to use clause
environments based on evars (fbbe491cfa157da627) *)
Require Import Setoid.
Parameter elt : Type.
Parameter T : Type -> Type.
Parameter empty : forall A, T A.
Parameter MapsTo : forall A : Type, elt -> A -> T A -> Prop.
(* Definition In A x t := exists e, MapsTo A x e t. *)
Axiom In : forall A, A -> T A -> Prop.
Axiom foo : forall A x, In A x (empty A) <-> False.
Record R := { t : T unit; s : unit }.
Definition Empty := {| t := empty unit; s := tt |}.
Goal forall x, ~ In _ x (t Empty).
Proof.
intros x.
rewrite foo.
Abort.
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
