Why Gemfury?
Push, build, and install
RubyGems
npm packages
Python packages
Maven artifacts
PHP packages
Go Modules
Debian packages
RPM packages
NuGet packages
duality-group
duality-group / Pygments python
Repository URL to install this package:
|
Version:
2.13.0 ▾
|
'domain' Keyword
' ' Text
'Option__Node' Name
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'unique' Keyword
' ' Text
'function' Keyword
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
':' Operator
' ' Text
'Option__Node' Name
'\n' Text
' ' Text
'unique' Keyword
' ' Text
'function' Keyword
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
':' Operator
' ' Text
'Option__Node' Name
'\n' Text
'\n' Text
' ' Text
'function' Keyword
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'self' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
':' Operator
' ' Text
'Option__Node' Name
'\n' Text
'\n' Text
' ' Text
'function' Keyword
' ' Text
'isOptionNode' Name
'(' Punctuation
'self' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
':' Operator
' ' Text
'Bool' Keyword.Type
'\n' Text
'\n' Text
' ' Text
'axiom' Keyword
' ' Text
'ax_variantOfOptionNodeChoices' Name
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'forall' Keyword
' ' Text
'x' Name
':' Operator
' ' Text
'Ref' Keyword.Type
' ' Text
':' Operator
':' Operator
' ' Text
'{ variantOfOptionNode(x) }' Generic.Emph
'\n' Text
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'x' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
' ' Text
'|' Operator
'|' Operator
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'x' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
'\n' Text
' ' Text
'axiom' Keyword
' ' Text
'ax_isCounterState' Name
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'forall' Keyword
' ' Text
'x' Name
':' Operator
' ' Text
'Ref' Keyword.Type
' ' Text
':' Operator
':' Operator
' ' Text
'{ variantOfOptionNode(x) }' Generic.Emph
'\n' Text
' ' Text
'isOptionNode' Name
'(' Punctuation
'x' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'x' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
' ' Text
'|' Operator
'|' Operator
'\n' Text
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'x' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'predicate' Keyword
' ' Text
'validOption' Name
'(' Punctuation
'this' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'isOptionNode' Name
'(' Punctuation
'this' Name
')' Punctuation
' ' Text
'&' Operator
'&' Operator
'\n' Text
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'this' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'(' Punctuation
'\n' Text
' ' Text
'acc' Keyword
'(' Punctuation
'this' Name
'.' Punctuation
'Option__Node__Some__1' Name
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
' ' Text
'&' Operator
'&' Operator
'\n' Text
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'field' Keyword
' ' Text
'Option__Node__Some__1' Name
':' Operator
' ' Text
'Ref' Keyword.Type
'\n' Text
'\n' Text
'field' Keyword
' ' Text
'Node__v' Name
':' Operator
' ' Text
'Int' Keyword.Type
'\n' Text
'field' Keyword
' ' Text
'Node__next' Name
':' Operator
' ' Text
'Ref' Keyword.Type
'\n' Text
'\n' Text
'predicate' Keyword
' ' Text
'validNode' Name
'(' Punctuation
'this' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'acc' Keyword
'(' Punctuation
'this' Name
'.' Punctuation
'Node__v' Name
')' Punctuation
' ' Text
'&' Operator
'&' Operator
'\n' Text
' ' Text
'acc' Keyword
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'&' Operator
'&' Operator
'\n' Text
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'\n' Text
'function' Keyword
' ' Text
'length' Name
'(' Punctuation
'this' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
':' Operator
' ' Text
'Int' Keyword.Type
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'result' Keyword
' ' Text
'>' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'(' Punctuation
'unfolding' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
' ' Text
'in' Keyword
'\n' Text
' ' Text
'unfolding' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
' ' Text
'in' Keyword
'\n' Text
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
')' Punctuation
' ' Text
'?' Operator
' \n ' Text
'1' Literal.Number.Integer
' ' Text
':' Operator
' ' Text
'1' Literal.Number.Integer
' ' Text
'+' Operator
' ' Text
'length' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
'\n' Text
' ' Text
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'function' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'this' Name
':' Operator
' ' Text
'Ref' Keyword.Type
',' Punctuation
' ' Text
'i' Name
':' Operator
' ' Text
'Int' Keyword.Type
')' Punctuation
':' Operator
' ' Text
'Int' Keyword.Type
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'0' Literal.Number.Integer
' ' Text
'<' Operator
'=' Operator
' ' Text
'i' Name
' ' Text
'&' Operator
'&' Operator
' ' Text
'i' Name
' ' Text
'<' Operator
' ' Text
'length' Name
'(' Punctuation
'this' Name
')' Punctuation
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'unfolding' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
' ' Text
'in' Keyword
' ' Text
'unfolding' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
' ' Text
'in' Keyword
' ' Text
'(' Punctuation
'\n' Text
' ' Text
'(' Punctuation
'i' Name
' ' Text
'=' Operator
'=' Operator
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'?' Operator
'\n' Text
' ' Text
'this' Name
'.' Punctuation
'Node__v' Name
':' Operator
'\n' Text
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
')' Punctuation
' ' Text
'?' Operator
' \n ' Text
'itemAt' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
',' Punctuation
' ' Text
'i' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
':' Operator
' ' Text
'this' Name
'.' Punctuation
'Node__v' Name
'\n' Text
' ' Text
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'function' Keyword
' ' Text
'sum' Name
'(' Punctuation
'this' Name
'$1' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
':' Operator
' ' Text
'Int' Keyword.Type
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
'$1' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'(' Punctuation
'unfolding' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
'$1' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
' ' Text
'in' Keyword
' ' Text
'unfolding' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'this' Name
'$1' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
' ' Text
'in' Keyword
' \n ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'this' Name
'$1' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
')' Punctuation
' ' Text
'?' Operator
' ' Text
'this' Name
'$1' Name
'.' Punctuation
'Node__v' Name
' ' Text
':' Operator
' ' Text
'this' Name
'$1' Name
'.' Punctuation
'Node__v' Name
' ' Text
'+' Operator
' ' Text
'sum' Name
'(' Punctuation
'this' Name
'$1' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'method' Keyword
' ' Text
'append' Name
'(' Punctuation
'this' Name
':' Operator
' ' Text
'Ref' Keyword.Type
',' Punctuation
' ' Text
'val' Name
':' Operator
' ' Text
'Int' Keyword.Type
')' Punctuation
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
' ' Text
'/*' Comment.Multiline
' POST1 ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'length' Name
'(' Punctuation
'this' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'(' Punctuation
'old' Keyword
'(' Punctuation
'length' Name
'(' Punctuation
'this' Name
')' Punctuation
')' Punctuation
' ' Text
'+' Operator
' ' Text
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'/*' Comment.Multiline
' POST2 ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'i' Name
':' Operator
' ' Text
'Int' Keyword.Type
' ' Text
':' Operator
':' Operator
' ' Text
'(' Punctuation
'0' Literal.Number.Integer
' ' Text
'<' Operator
'=' Operator
' ' Text
'i' Name
' ' Text
'&' Operator
'&' Operator
' ' Text
'i' Name
' ' Text
'<' Operator
' ' Text
'old' Keyword
'(' Punctuation
'length' Name
'(' Punctuation
'this' Name
')' Punctuation
')' Punctuation
')' Punctuation
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'(' Punctuation
'itemAt' Name
'(' Punctuation
'this' Name
',' Punctuation
' ' Text
'i' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'old' Keyword
'(' Punctuation
'itemAt' Name
'(' Punctuation
'this' Name
',' Punctuation
' ' Text
'i' Name
')' Punctuation
')' Punctuation
')' Punctuation
')' Punctuation
' ' Text
'/*' Comment.Multiline
' POST3 ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'itemAt' Name
'(' Punctuation
'this' Name
',' Punctuation
' ' Text
'length' Name
'(' Punctuation
'this' Name
')' Punctuation
' ' Text
'-' Operator
' ' Text
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'val' Name
' ' Text
'/*' Comment.Multiline
' POST4 ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'true' Keyword
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'true' Keyword
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'tmp_node' Name
':' Operator
' ' Text
'Ref' Keyword.Type
'\n' Text
' ' Text
'var' Keyword
' ' Text
'tmp_option' Name
':' Operator
' ' Text
'Ref' Keyword.Type
'\n' Text
'\n' Text
' ' Text
'unfold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'unfold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
'\n' Text
' ' Text
'if' Keyword
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
')' Punctuation
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'tmp_node' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'new' Keyword
'(' Punctuation
'Node__next' Name
',' Punctuation
' ' Text
'Node__v' Name
')' Punctuation
'\n' Text
' ' Text
'tmp_node' Name
'.' Punctuation
'Node__next' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'null' Keyword
'\n' Text
' ' Text
'tmp_node' Name
'.' Punctuation
'Node__v' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'val' Name
'\n' Text
'\n' Text
' ' Text
'assume' Keyword
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'tmp_node' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'tmp_node' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'tmp_node' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
'\n' Text
' ' Text
'tmp_option' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'new' Keyword
'(' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
'\n' Text
' ' Text
'tmp_option' Name
'.' Punctuation
'Option__Node__Some__1' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'tmp_node' Name
'\n' Text
' ' Text
'assume' Keyword
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'tmp_option' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'tmp_option' Name
')' Punctuation
')' Punctuation
'\n' Text
'\n' Text
' ' Text
'this' Name
'.' Punctuation
'Node__next' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'tmp_option' Name
'\n' Text
'\n' Text
' \n ' Text
'unfold' Keyword
' ' Text
'validOption' Name
'(' Punctuation
'tmp_option' Name
')' Punctuation
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'length' Name
'(' Punctuation
'tmp_node' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
' ' Text
'/*' Comment.Multiline
' TODO: Required by Silicon, POST2 fails otherwise ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'tmp_node' Name
',' Punctuation
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'val' Name
' ' Text
'/*' Comment.Multiline
' TODO: Required by Silicon, POST4 fails otherwise ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'validOption' Name
'(' Punctuation
'tmp_option' Name
')' Punctuation
'\n' Text
' ' Text
'}' Punctuation
' ' Text
'else' Keyword
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'append' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
',' Punctuation
' ' Text
'val' Name
')' Punctuation
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'this' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'this' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'method' Keyword
' ' Text
'prepend' Name
'(' Punctuation
'tail' Name
':' Operator
' ' Text
'Ref' Keyword.Type
',' Punctuation
' ' Text
'val' Name
':' Operator
' ' Text
'Int' Keyword.Type
')' Punctuation
' ' Text
'returns' Keyword
' ' Text
'(' Punctuation
'res' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'tail' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'res' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'//ensures acc(validNode(tail))\n' Comment.Single
' ' Text
'ensures' Name.Decorator
' ' Text
'length' Name
'(' Punctuation
'res' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'old' Keyword
'(' Punctuation
'length' Name
'(' Punctuation
'tail' Name
')' Punctuation
')' Punctuation
' ' Text
'+' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'i' Name
':' Operator
' ' Text
'Int' Keyword.Type
' ' Text
':' Operator
':' Operator
' ' Text
'(' Punctuation
'1' Literal.Number.Integer
' ' Text
'<' Operator
'=' Operator
' ' Text
'i' Name
' ' Text
'&' Operator
'&' Operator
' ' Text
'i' Name
' ' Text
'<' Operator
' ' Text
'length' Name
'(' Punctuation
'res' Name
')' Punctuation
')' Punctuation
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'(' Punctuation
'itemAt' Name
'(' Punctuation
'res' Name
',' Punctuation
' ' Text
'i' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'old' Keyword
'(' Punctuation
'itemAt' Name
'(' Punctuation
'tail' Name
',' Punctuation
' ' Text
'i' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
')' Punctuation
')' Punctuation
')' Punctuation
' ' Text
'/*' Comment.Multiline
' POST3 ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'itemAt' Name
'(' Punctuation
'res' Name
',' Punctuation
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'val' Name
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'tmp_option' Name
':' Operator
' ' Text
'Ref' Keyword.Type
'\n' Text
'\n' Text
' ' Text
'res' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'new' Keyword
'(' Punctuation
'Node__v' Name
',' Punctuation
' ' Text
'Node__next' Name
')' Punctuation
'\n' Text
' ' Text
'res' Name
'.' Punctuation
'Node__v' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'val' Name
'\n' Text
'\n' Text
' ' Text
'tmp_option' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'new' Keyword
'(' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
'\n' Text
' ' Text
'tmp_option' Name
'.' Punctuation
'Option__Node__Some__1' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'tail' Name
'\n' Text
' ' Text
'assume' Keyword
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'tmp_option' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
'\n' Text
'\n' Text
' ' Text
'res' Name
'.' Punctuation
'Node__next' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'tmp_option' Name
'\n' Text
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'tail' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'res' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'res' Name
')' Punctuation
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'method' Keyword
' ' Text
'length_iter' Name
'(' Punctuation
'list' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
' ' Text
'returns' Keyword
' ' Text
'(' Punctuation
'len' Name
':' Operator
' ' Text
'Int' Keyword.Type
')' Punctuation
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'list' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'old' Keyword
'(' Punctuation
'length' Name
'(' Punctuation
'list' Name
')' Punctuation
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'len' Name
'\n' Text
' ' Text
'// TODO we have to preserve this property\n' Comment.Single
' ' Text
'// ensures acc(validNode(list))\n' Comment.Single
'{' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'curr' Name
':' Operator
' ' Text
'Ref' Keyword.Type
' ' Text
':' Operator
'=' Operator
' ' Text
'list' Name
'\n' Text
' ' Text
'var' Keyword
' ' Text
'tmp' Name
':' Operator
' ' Text
'Ref' Keyword.Type
' ' Text
':' Operator
'=' Operator
' ' Text
'list' Name
'\n' Text
'\n' Text
' ' Text
'len' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
'\n' Text
' ' Text
'unfold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'curr' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'unfold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'while' Keyword
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'invariant' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__v' Name
')' Punctuation
'\n' Text
' ' Text
'invariant' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
'\n' Text
' ' Text
'invariant' Name.Decorator
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'(' Punctuation
'\n' Text
' ' Text
'acc' Keyword
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
' ' Text
'&' Operator
'&' Operator
'\n' Text
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'invariant' Name.Decorator
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__Some' Name
'(' Punctuation
')' Punctuation
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'len' Name
' ' Text
'+' Operator
' ' Text
'length' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'old' Keyword
'(' Punctuation
'length' Name
'(' Punctuation
'list' Name
')' Punctuation
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'invariant' Name.Decorator
' ' Text
'(' Punctuation
'variantOfOptionNode' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'len' Name
' ' Text
'=' Operator
'=' Operator
' ' Text
'old' Keyword
'(' Punctuation
'length' Name
'(' Punctuation
'list' Name
')' Punctuation
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'len' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'len' Name
' ' Text
'+' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
' ' Text
'tmp' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'curr' Name
'\n' Text
' ' Text
'curr' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'curr' Name
'.' Punctuation
'Node__next' Name
'.' Punctuation
'Option__Node__Some__1' Name
'\n' Text
' ' Text
'unfold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'curr' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'unfold' Keyword
' ' Text
'acc' Keyword
'(' Punctuation
'validOption' Name
'(' Punctuation
'curr' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
')' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'method' Keyword
' ' Text
't1' Name
'(' Punctuation
')' Punctuation
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'l' Name
':' Operator
' ' Text
'Ref' Keyword.Type
'\n' Text
'\n' Text
' ' Text
'l' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'new' Keyword
'(' Punctuation
'Node__v' Name
',' Punctuation
' ' Text
'Node__next' Name
')' Punctuation
'\n' Text
' ' Text
'l' Name
'.' Punctuation
'Node__next' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'null' Keyword
'\n' Text
' ' Text
'l' Name
'.' Punctuation
'Node__v' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
' ' Text
'assume' Keyword
' ' Text
'variantOfOptionNode' Name
'(' Punctuation
'l' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'Option__Node__None' Name
'(' Punctuation
')' Punctuation
'\n' Text
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'validOption' Name
'(' Punctuation
'l' Name
'.' Punctuation
'Node__next' Name
')' Punctuation
'\n' Text
' ' Text
'fold' Keyword
' ' Text
'validNode' Name
'(' Punctuation
'l' Name
')' Punctuation
'\n' Text
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'length' Name
'(' Punctuation
'l' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
'\n' Text
' ' Text
'append' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'7' Literal.Number.Integer
')' Punctuation
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'7' Literal.Number.Integer
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'length' Name
'(' Punctuation
'l' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'2' Literal.Number.Integer
'\n' Text
'\n' Text
' ' Text
'l' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'prepend' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'10' Literal.Number.Integer
')' Punctuation
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'2' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'7' Literal.Number.Integer
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'1' Literal.Number.Integer
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'itemAt' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'10' Literal.Number.Integer
'\n' Text
' ' Text
'assert' Keyword
' ' Text
'length' Name
'(' Punctuation
'l' Name
')' Punctuation
' ' Text
'=' Operator
'=' Operator
' ' Text
'3' Literal.Number.Integer
'\n' Text
'\n' Text
' ' Text
'//assert sum(l) == 18\n' Comment.Single
'}' Punctuation
'\n' Text
'\n' Text
'method' Keyword
' ' Text
't2' Name
'(' Punctuation
'l' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
' ' Text
'returns' Keyword
' ' Text
'(' Punctuation
'res' Name
':' Operator
' ' Text
'Ref' Keyword.Type
')' Punctuation
'\n' Text
' ' Text
'requires' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'l' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'acc' Keyword
'(' Punctuation
'validNode' Name
'(' Punctuation
'res' Name
')' Punctuation
',' Punctuation
' ' Text
'write' Keyword
')' Punctuation
'\n' Text
' ' Text
'ensures' Name.Decorator
' ' Text
'length' Name
'(' Punctuation
'res' Name
')' Punctuation
' ' Text
'>' Operator
' ' Text
'old' Keyword
'(' Punctuation
'length' Name
'(' Punctuation
'l' Name
')' Punctuation
')' Punctuation
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'res' Name
' ' Text
':' Operator
'=' Operator
' ' Text
'prepend' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'10' Literal.Number.Integer
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text