|
Record t := {x : bool; y : bool; z : bool}.
Goal forall x1 x2 y z,
{| x := x1; y := y; z := z |} = {| x := x2; y := y; z := z |} -> x1 = x2.
Proof.
intros; congruence. (* was doing stack overflow *)
Qed.
¤ Dauer der Verarbeitung: 0.15 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.
|
