|
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.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.21Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
