diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 15:47:24 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 15:49:42 +0100 |
| commit | 51b4d0cdad77f2874bd481dabd32e0772563dc3f (patch) | |
| tree | ec813c0fc816ca1446ef70e68151cdb889646f58 /test-suite | |
| parent | ac62cda8a4f488b94033b108c37556877232137a (diff) | |
Fix bug #4103: forgot to allow unfolding projections of cofixpoints like
cases, in some cases.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4103.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4103.v b/test-suite/bugs/closed/4103.v new file mode 100644 index 000000000..92cc0279a --- /dev/null +++ b/test-suite/bugs/closed/4103.v @@ -0,0 +1,12 @@ +Set Primitive Projections. + +CoInductive stream A := { hd : A; tl : stream A }. + +CoFixpoint ticks (n : nat) : stream unit := {| hd := tt; tl := ticks n |}. + +Lemma expand : exists n : nat, (ticks n) = (ticks n).(tl _). +Proof. + eexists. + (* Set Debug Tactic Unification. *) + (* Set Debug RAKAM. *) + reflexivity. |