In 8.2.3.2 "Implicit Completion Values",
the first equivalence says that
1. Return the String "Infinity".
means the same thing as:
1. Return Completion {[[type]]: normal, [[value]]: String "Infinity",
[[target]]:empty}.
Since you've just defined 'NormalCompletion', you could replace the latter line with just:
1. Return NormalCompletion(String "Infinity")
---
Also, instead of it being an example (involving the string "Infinity"), you could make it a general statement:
1. Return argument.
means
1. Return NormalCompletion(argument).
corrected in rev 13 editor's draft
at least the first suggestion. I think I like the example form in this case