Hacker News new | ask | show | jobs
by chriswarbo 2667 days ago
I think this is the mathematical/logical distinction between "object level" and "meta level".

The meta level is about lambda terms, involving things like variable names, abstractions, judgements, derivations, equivalences, reductions, substitutions, etc.

The object level is what lambda terms are about, involving things like values, types, variable contents, etc.