Record T : Type := Build_T { f : unit; g := pair f f; }.
Definition t : T := {| f := tt; |}.
Goalmatch t return unit with Build_T f g => f end = tt. Proof.
cbv. reflexivity. Qed.
Goalmatch t return prod unit unit with Build_T f g => g end = pair tt tt. Proof.
cbv. reflexivity. Qed.
Goalforall (x : T), match x return prod unit unit with Build_T f g => g end =
pair match x return unit with Build_T f g => fst g endmatch x return unit with Build_T f g => snd g end. Proof.
cbv. destruct x. reflexivity. Qed.
Record U : Type := Build_U { h := tt }.
Definition u : U := Build_U.
Goalmatch u with Build_U h => h end = tt. Proof.
cbv. reflexivity. Qed.
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.
