Skip to main content


Entrypoints' effect may call functions. A function returns a value, may fail, and can change the contract storage.

A function is declared with the function keyword followed by a unique identifier.


A function may return a value; it then uses the return keyword. The return type is specified after the function arguments declaration, followed by :.

For example, the following function implements the Horner's formula of the exponential function:

function exp(x : rational, steps : nat) : rational {
var r : rational = 1 + x / steps;
iter i to steps - 1 do
r := 1 + x * r / (steps - i)
return r

When the function does not change the storage, it is compiled as a lambda expression on the stack. When the function does change the storage, it is inlined.

Function as instruction

The return value, and the return type declaration, are optional. In that case, the function is considered as an instruction. For example, the function set_res below simply assigns a value to a storage variable:

archetype example

variable res : nat = 0

function set_res(v : nat) {
res := v

entry exec() {

Such functions are inlined, even if they do not change the contract's storage.

Inlining strategy

A function that does not modify the storage nor emit operations is inlined. Any other function is compiled as a lambda expression.

In views a function is always inlined.