namespace Main(16);
    // Returns folder(...folder(folder(0, f(0)), f(1)) ..., f(length - 1))
    // This is a generic function.
    let<T1, T2> fold: int, (int -> T1), T2, (T2, T1 -> T2) -> T2 =
        |length, f, initial, folder| match length {
            0 => initial,
            _ => folder(fold(length - 1, f, initial, folder), f(length - 1))
        };
    // returns f(0) + f(1) + ... + f(length - 1)
    let sum = |length, f| fold(length, f, 0, |acc, e| acc + e);
    // This function takes an algebraic expression (a column or expression
    // involving columns) and returns an identity that forces this expression
    // to equal 20. Note that `=` is not an assignment but creates an identity constraint.
    let equals_twenty: expr -> Constr = |x| x = 20;
    // This declares an array of 16 witness columns.
    col witness wit[16];
    // This expression has to evaluate to an identity, but we can still use
    // higher order functions and all the flexibility of the language.
    // The sub-expression `sum(16, |i| wit[i])` evaluates to the algebraic
    // expression "wit[0] + wit[1] + ... + wit[15]", which is then
    // turned into the identity by `equals_twenty`
    // wit[0] + wit[1] + ... + wit[15] = 20.
    equals_twenty(sum(16, |i| wit[i]));

    // We constrained the sum to equal twenty, but there is no unique solution
    // to that constraint. In order to fully constrain the system, we need to
    // add something more: The first fifteen columns should all be one.

    // returns [f(0), f(1), ..., f(length - 1)]
    let make_array = |length, f| fold(length, f, [], |acc, e| acc + [e]);
    // If an expression evaluates to an array of constraints, all the
    // constraints in the array are added to the system.
    make_array(15, |i| wit[i] = 1);