Is it safe to let `synth` return `Value` (for type) and `Core` (for exp) instead of `Core` and `Core`?

[xieyuheng]

By doing so, we can avoid some repeated readback and evaluate in synth.

[david-christiansen]

Yes, absolutely. We thought it would be easier to see the correspondence between the implementation and the rules in the back of the book if if returned expressions, but returning values is a better way to make a fast implementation. I also think it's conceptually better for various reasons.