blob: cb39893f47054003b8915866b253f3ac5e553afa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* 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).
|
