(* A bug in the guard checking of nested cofixpoints. *) (* Posted by Maxime Dénès on coqdev (Apr 9, 2014). *)
CoInductive CoFalse := .
CoInductive CoTrue := I.
Fail CoFixpoint loop : CoFalse :=
(cofix f := loop with g := loop for f).
Fail CoFixpoint loop : CoFalse :=
(cofix f := I with g := loop for g).
Fail CoFixpoint loop : CoFalse :=
(cofix f := loop with g := I for f).
Messung V0.5
¤ 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.0.9Bemerkung:
(vorverarbeitet)
¤
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 und die Messung sind noch experimentell.