|
Set Primitive Projections.
Record foo := Foo {
foo_car : Type;
foo_rel : foo_car -> foo_car -> Prop
}.
Arguments foo_rel : simpl never.
Definition foo_fun {A B} := Foo (A -> B) (fun f g => forall x, f x = g x).
Goal @foo_rel foo_fun (fun x : nat => x) (fun x => x).
Proof.
intros x; exact eq_refl.
Undo.
progress hnf; intros; exact eq_refl.
Undo.
unfold foo_rel. intros x. exact eq_refl.
Qed.
¤ Dauer der Verarbeitung: 0.16 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.
|
