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.
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