|
(* Bugs in computing dependencies in pattern-matching compilation *)
Inductive A := a1 | a2.
Inductive B := b.
Inductive C : A -> Type := c : C a1 | d : C a2.
Definition P (x : A) (y : C x) (z : B) : nat :=
match z, x, y with
| b, a1, c => 0
| b, a2, d => 0
| _, _, _ => 1
end.
¤ Dauer der Verarbeitung: 0.16 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.
|
