|
Set Primitive Projections.
Polymorphic Record pair {A B : Type} : Type :=
prod { pr1 : A; pr2 : B }.
Notation " ( x ; y ) " := (@prod _ _ x y).
Notation " x .1 " := (pr1 x) (at level 3).
Notation " x .2 " := (pr2 x) (at level 3).
Goal ((0; 1); 2).1.2 = 1.
Proof.
cbv.
match goal with
| |- ?t = ?t => exact (eq_refl t)
end.
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.
|
