Currently, the type of the _Await syntax constant states that Await works with program continuations, when in fact it works with program option continuations. Apparently, this mismatch isn’t spotted by Isabelle, and it also doesn’t seem to cause problems. We shall fix the type of _Await nevertheless. We shall also change the identifier used for the final term in the syntax translation accordingly.
Currently, the type of the
_Awaitsyntax constant states thatAwaitworks with program continuations, when in fact it works with program option continuations. Apparently, this mismatch isn’t spotted by Isabelle, and it also doesn’t seem to cause problems. We shall fix the type of_Awaitnevertheless. We shall also change the identifier used for the final term in the syntax translation accordingly.