Skip to content

Commit 22c05f8

Browse files
committed
no functions in K
1 parent 819da1d commit 22c05f8

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

erc20.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,8 @@ these functions.
9494
However, K is a general purpose framework and makes no implicit assumptions,
9595
so we have to say it explicitly that expressions are allowed to be passed as
9696
arguments.
97+
In fact, K does not even know that these language constructs are meant to be
98+
"functions", nor even what a function is by default.
9799

98100
All ERC20 functions above that take arguments have the attribute `strict`,
99101
which in K means that they should first evaluate their arguments.

0 commit comments

Comments
 (0)