Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }. Arguments pair {_ _} _ _. Notation"( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Definition ap11 {A B} {f g:A->B} (h:f=g) {x y:A} (p:x=y) : f x = g y. Admitted. Goalforall x y z w : Set, (x, y) = (z, w). Proof. intros. apply ap11. (* Toplevel input, characters 21-25: Error:Inenvironment x:Set y:Set z:Set w:Set Unabletounify"?31?191=?32?192"with"(x,y)=(z,w)".
*) Abort.
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-09-29)
¤
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 und die Messung sind noch experimentell.
