You may be using an older version of scribble. Earlier scribble allowed annotations without a leading #
- e.g. invariant x > 0;
instead of #invariant x > 0
. However we found that since some of the keywords we use (e.g. invariant
and define
) can occur in normal docstrings, sometimes scribble can get confused and try and treat something that is not an annotation as an annotation. To solve this problem we made the #
required. So try to upgrade scribble to the latest version, and make sure all your annotations start with #
.