bench: invalid goal for induction_pr

72f7ddbc · Jean-Christophe Filliâtre · 5446ded9 · 72f7ddbc
Commit 72f7ddbc authored Sep 22, 2014 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 10 additions and 0 deletions

bench/invalid/induction.mlw bench/invalid/induction.mlw +10 -0

No files found.
--- a/bench/invalid/induction.mlw
+++ b/bench/invalid/induction.mlw
+
+module M
+
+  coinductive p unit =
+  | C: p () -> p ()
+
+  (* should not be proved using induction_pr *)
+  goal G: p () -> false
+
+end