@Cameron-Low , could we have a codepos for "after the last line"? I assume that "before the last line + 1" would already work here? _Originally posted by @fdupress in https://github.com/EasyCrypt/easycrypt/issues/773#issuecomment-2858760912_