From ea6826991055b83935c8055cdaccceb5680d13db Mon Sep 17 00:00:00 2001
From: Octavian-Eugen Ganea <octavian-eugen.ganea@epfl.ch>
Date: Thu, 24 Mar 2011 00:57:35 +0000
Subject: [PATCH]
---
testcases/Naturals.scala | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/testcases/Naturals.scala b/testcases/Naturals.scala
index 8b626b672..8f9ea8315 100644
--- a/testcases/Naturals.scala
+++ b/testcases/Naturals.scala
@@ -33,6 +33,10 @@ object Naturals {
plus(Zero(), x) == plus(x, Zero())
} holds
+
+// induction is made on first parameter
+//induction on x works here!
+//induction on y = stack overflow
@induct
def oneCommut(x : Nat, y : Nat) : Boolean = {
Succ(plus(x,y)) == plus(x, Succ(y))
--
GitLab