// A tiny lexical bug in an error report, - not followed.
module LexicalPopBug
#push-options "--split_queries always"
let oneisone ():
Lemma (ensures 1 = 1)
= ()
#pop-option
/// * Error 72 at src/LexicalPopBug.fst(8,1-8,4):
/// - Identifier not found: [pop] [2 times]
/// instead of pop-option.