14.2. Assertion Logic: some arrows should be single-lined about frap HOT 3 CLOSED

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.

from frap.

@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).

from frap.

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.

from frap.