Skip to content

Commit 3c4f314

Browse files
ttuegelehildenb
authored andcommitted
Add functional attribute to #sizeWordStack (#400)
1 parent 5b9a3a0 commit 3c4f314

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

data.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -456,9 +456,9 @@ A cons-list is used for the EVM wordstack.
456456
- `_in_` determines if a `Int` occurs in a `WordStack`.
457457

458458
```k
459-
syntax Int ::= #sizeWordStack ( WordStack ) [function, smtlib(sizeWordStack)]
460-
| #sizeWordStack ( WordStack , Int ) [function, klabel(sizeWordStackAux), smtlib(sizeWordStackAux)]
461-
// ----------------------------------------------------------------------------------------------------------------
459+
syntax Int ::= #sizeWordStack ( WordStack ) [function, functional, smtlib(sizeWordStack)]
460+
| #sizeWordStack ( WordStack , Int ) [function, functional, klabel(sizeWordStackAux), smtlib(sizeWordStackAux)]
461+
// ----------------------------------------------------------------------------------------------------------------------------
462462
rule #sizeWordStack ( WS ) => #sizeWordStack(WS, 0)
463463
rule #sizeWordStack ( .WordStack, SIZE ) => SIZE
464464
rule #sizeWordStack ( W : WS, SIZE ) => #sizeWordStack(WS, SIZE +Int 1)

0 commit comments

Comments
 (0)