// string = expr.to_string() + "\n\n~~>\n\n";
string = '';
eta = document.getElementById('ETA').checked;
- string = string + reduce(expr, eta, 2).to_string();
+ string = string + reduce(expr, eta, 1).to_string();
} catch (e) {
string = JSON.stringify(e, ['name', 'message', 'from', 'to', 'key',
'value', 'arity', 'first', 'second', 'third', 'fourth'], 4);