(* An example showing a bug in the detection of free variables *) (* "x" is not free in the common type of "x" and "y" *)
Checkforall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
(* An example showing a bug in the detection of bound variables *)
Goalforall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl. intro. matchgoalwith
|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end. intro. Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *) Abort.
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.
