diff --git a/testcases/Naturals.scala b/testcases/Naturals.scala index 8b626b67276e71687fda7f265cefb15c8c8397c4..8f9ea83156cc9ea3d37652b33dacf74ae387fe06 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))