FAQ

1.I'm seeing a syntax error in a docstring where there is no annotation. What gives?
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 #.

  2. I'm getting an error "TypeError: Variable ... is defined in the new context in ... but used in an old() expression"
See this section for help.
​
​
Last modified 8mo ago