|
(* This used to raise an anomaly in 8.4 and trunk up to 17 April 2013 *)
Set Implicit Arguments.
Inductive path (V : Type) (E : V -> V -> Type) (s : V) : V -> Type :=
| NoEdges : path E s s
| AddEdge : forall d d' : V, path E s d -> E d d' -> path E s d'.
Inductive G_Vertex := G_v0 | G_v1.
Inductive G_Edge : G_Vertex -> G_Vertex -> Set := G_e : G_Edge G_v0 G_v1.
Goal forall x1 : G_Edge G_v1 G_v1, @AddEdge _ G_Edge G_v1 _ _ (NoEdges _ _) x1 = NoEdges _ _.
intro x1.
try destruct x1. (* now raises a typing error *)
Abort.
¤ 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.
|
