Functions

A function declares its clauses in a fixed order. The return type is required; there is no inference. Effects, preconditions, postconditions, and the termination measure are all part of the signature and all checked.

function read_at(rfs: ReadOnlyFilesystem, path: String, offset: u64, len: usize, allocator: Allocator) -> [u8]
    with {rfs, allocator, err: fs.FsError}
    requires len > 0
    ensures  result.len() <= len
{
    ...
}

Inside ensures, result names the return value. Edda admits no comments of any kind; a claim about the code lives in the effect row, a refinement, or an attribute, where a check can hold it true. Descriptions are derived into the structure map, not written by hand.