|
Set Primitive Projections.
Record foo : Type := bar { x : unit }.
Goal forall t u, bar t = bar u -> t = u.
Proof.
intros.
injection H.
trivial.
Qed.
(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *)
(** Dependent pattern-matching is ok on this one as it has eta *)
Definition baz (x : foo) :=
match x as x' return x' = x' with
| bar u => eq_refl
end.
Inductive foo' : Type := bar' {x' : unit; y: foo'}.
(** Dependent pattern-matching is not ok on this one *)
Fail Definition baz' (x : foo') :=
match x as x' return x' = x' with
| bar' u y => eq_refl
end.
¤ Dauer der Verarbeitung: 0.15 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.
|
