Closed PetarMax closed 9 years ago
Hi,
We should be using "abrupt_res R" everywhere, first to avoid negation, and second because it's the terminology used in ecma.
Thanks! + Arthur
In JsSyntax.v: 676 we define abrupt_res as a completion triple the type of which is not normal, but we don't use this definition onward.
On the other hand, in JsPrettyInterm.v:1369 we define res_is_normal as the opposite of abrupt_res, and later use it mostly in contexts in which it is negated.
I guess we could get rid of one of them and update the development accordingly?
— Reply to this email directly or view it on GitHub https://github.com/resource-reasoning/jscert_dev/issues/13.
In JsSyntax.v: 676 we define abrupt_res as a completion triple the type of which is not normal, but we don't use this definition onward.
On the other hand, in JsPrettyInterm.v:1369 we define res_is_normal as the opposite of abrupt_res, and later use it mostly in contexts in which it is negated.
I guess we could get rid of one of them and update the development accordingly?