|
Set Primitive Projections.
Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }.
Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True.
Proof.
set (Q1 := total2 (fun f => pr1 P f = x)).
set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)).
Abort.
¤ Dauer der Verarbeitung: 0.20 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.
|
