14.2. Assertion Logic: some arrows should be single-lined

[p0llard]

Following the text:

We can also define natural comparison operators between assertions, overload-
ing the usual notations for equivalence and implication of propositions.

I believe that the arrows on the right hand side of the equality should be single-lined arrows, not double, since they are implication and equivalence in the meta-language, not the object language, but I might be mistaken.

[achlipala]

I think the convention I'm following in the book is to use double arrows for metalanguage implications. The only single arrows I found, searching just now (admittedly not very thoroughly), are for operational-semantics small-step relations. This is different from Coq notation, but I think it's consistent.

Yes, the double arrows you're referencing follow overloaded notation to apply both to normal propositions and to separation-logic assertions -- which is standard practice, but which might still deserve some clarification.

[p0llard]

@achlipala Perhaps the first inference rule immediately below this should be altered then? This seems to use a single arrow for metalanguage implication (which is what prompted me to raise this).

[achlipala]

Oh, yes, I agree that's inconsistent. That does seem to be the only use of a single right arrow for implication in the book at the moment. Let me correct it.