FStar
FStar copied to clipboard
Tiny lexical issue in error 72
// 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.