Correct. I think of it this way: The reduction rules prescribe an encoding for functions, but don't describe it for other (traditional) data. But there are very

Correct. I think of it this way: The reduction rules prescribe an encoding for functions, but don't describe it for other (traditional) data. But there are very canonical choices of course, which the demos on the website follow: * false := t and true := t t * Pairs are t first_elem second_elem * Lists could be encoded as (t first_elem (t second_elem (t third_elem ...))) with empty list being t * Natural numbers as lists of booleans (LSB first) * Strings as lists of natural numbers (unicode code points) These choices will affect what the functions that operate on data look like, concretely.