What (if any) is the difference between a lemma and ghost method. I was under the impression that they are both the same but calling a ghost method from a lemma throws the following error in a hint, calls are allowed only to lemmas, i.e.
ghost method foo ...
lemma bar ..
..
calc {
{foo ..;} // <--- ERROR!
}
A lemma is semantically the same as a ghost method. For example, in a location where a method may be called, such as a statement in a block statement within a method, it does not matter whether a lemma is relabled as a ghost method.
However, it appears that in some situations, such as the block of statements in an assert-by statement or a calc statement, Dafny currently insists that a ghost method be specifically called a lemma. And calling it a lemma more clearly communicates its purpose to readers.
I'll enter an Issue for the Dafny developers to ask whether this behavior is desired, but for now just call it a lemma if you are going to use it in calc and similar statements.