diff options
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/bug_3282.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_3282.v b/test-suite/bugs/closed/bug_3282.v index ce7cab1cba..f32e0969c8 100644 --- a/test-suite/bugs/closed/bug_3282.v +++ b/test-suite/bugs/closed/bug_3282.v @@ -5,3 +5,25 @@ Definition foo := fix f (m : nat) (o := true) (n : nat) {struct n} := Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := match n with 0 => 0 | S n' => f 0 n' end. + +Definition foo' := fix f {m : nat} (o := true) (n : nat) {struct n} := + match n with 0 => 0 | S n' => f (m:=0) n' end. +Check foo' (m:=0) 0. + +Fixpoint f' {m : nat} (o := true) (n : nat) {struct n} := + match n with 0 => 0 | S n' => f' (m:=0) n' end. +Check f' (m:=0) 0. + +CoInductive Stream := { hd : nat; tl : Stream }. + +Definition cofoo := cofix f (o := true) {m} := {| hd := 0; tl := f (m:=0) |}. +Check cofoo (m:=0). + +CoFixpoint cof (o := true) {m} := {| hd := 0; tl := cof (m:=0) |}. +Check cof (m:=0). + +Definition cofoo' := cofix f {m} (o := true) := {| hd := 0; tl := f (m:=0) |}. +Check cofoo' (m:=0). + +CoFixpoint cof' {m} (o := true) := {| hd := 0; tl := cof' (m:=0) |}. +Check cof' (m:=0). |