@lexi.lambda When you have something like (eval:check (+ 1 2) 3), the (+ 1 2) part is evaluated by itself and rendered, with the side-effect of the : Integer output that you expect. Then, 3 is evaluated, so its result can be compared to the result of (+ 1 2); in the process of evaluating3`, another ": Integer" is printed, but that printout stays in the output buffer until a later rendering reads from it.

Possible changes to eval:check include (1) waiting until after the second expression is evaluated to gather output; (2) discarding any output from the second expression. Either of those options would be less confusing than the current behavior, and I lean toward option (1), but that would mean you need to wrap expected-result expressions in some way so that they don’t produce output.

@mflatt Oh, of course. I should have realize what was going on there. Thanks.

@mflatt Finally got around to implementing your local-expand + trampolining solution, and it looks like it works well. Thanks for your help. :)