Set Primitive Projections. SetImplicitArguments.
Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. Definition eta_sigma {A} {P : A -> Type} (u : sigT P)
: existT _ (projT1 u) (projT2 u) = u
:= match u with existT _ x y => eq_refl end. (* Toplevel input, characters 0-139: Error: Pattern-matching expression on an object of inductive type sigT
has invalid information. *) Definition sum_of_sigT A B (x : sigT (fun b : bool => if b then A else B))
: A + B
:= match x with
| existT _ true a => inl a
| existT _ false b => inr b end. (* Toplevel input, characters 0-182: Error: Pattern-matching expression on an object of inductive type sigT
has invalid information. *)
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.
