8 Checked Bodies🔗ℹ

The bodies of functions with refinements can use many but not all features of Shplait. A body is a sequence of (zero or more) local defs followed by one result expression, and it may contain:

• integer, boolean and symbol literals, and identifiers;

• +, -, *, /, mod, comparisons, &&, || and !;

• if, cond, match and let;

• calls to this module’s functions and constructors;

• the builtins max, min, add1, sub1, is_even, is_odd, the list and string measures, and cons;

• error, unreachable and assert (error, unreachable and assert).

For instance, there is no abs; write max(n, -n). A local def may not shadow a parameter or an earlier local.