inductive predicates

Feb 10, 2017 at 2:19 PM
Edited Feb 10, 2017 at 2:21 PM
I guess that Dafny syntax doesn't allow to declare auxiliary variables in the body of inductive predicates, does it? why?