We may at some point want to implement lazy evaluation:

• I believe it would be necessary to support recursive definitions (Add letrec terms #469)
• Could make elaboration faster by avoiding unnecessary evaluation

I tried to copy the LazyValue implementation from Pikelet, but LazyValue uses OnceCell, which makes Value invariant over its 'arena lifetime, and introduces lifetime errors everywhere. Not sure if they can be fixed, or if we can implement lazy evaluation some other way