|
Set Primitive Projections.
Set Implicit Arguments.
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. *)
¤ Dauer der Verarbeitung: 0.14 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.
|
