Set Universe Polymorphism. Set Printing All. SetImplicitArguments.
Record prod A B := pair { fst : A ; snd : B }. Goalforall x : prod SetSet, let f := @fst _ in f _ x = @fst _ _ x. simpl; intros.
constr_eq (@fst SetSet x) (fst (A := Set) (B := Set) x).
Fail progress change (@fst SetSet x) with (fst (A := Set) (B := Set) x). 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.
