blob: e7a671ab482bb3198517751a37714050851e7071 (
plain)
1
2
3
4
5
6
|
constructors-cause-matching-loops.dfy(10,9): Info: Selected triggers: {Succ(s)}
Rejected triggers:
{f(s)} (may loop with "f(Succ(s))")
{f(Succ(s))} (more specific than {Succ(s)})
Dafny program verifier finished with 3 verified, 0 errors
|
