|
Require Import Setoid Program.Basics.
Parameter P : nat -> Prop.
Parameter R : nat -> nat -> Prop.
Add Parametric Morphism : P
with signature R ++> impl as PM1.
Admitted.
Add Parametric Morphism : P
with signature R --> impl as PM2.
Admitted.
Goal forall x y, R x y -> P y -> P x.
Proof.
intros x y H1 H2.
rewrite H1.
auto.
Qed.
¤ Dauer der Verarbeitung: 0.17 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.
|
