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