I don't believe the original performs NbE. It _looks_ like NbE, but the composition of `eval` and `quote` will not give you beta-normal forms. `quote` explicitl

I don't believe the original performs NbE. It _looks_ like NbE, but the composition of `eval` and `quote` will not give you beta-normal forms. `quote` explicitly wraps inferrable terms in `Inf`, while `eval` eliminates `Inf`.