FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Tiny lexical issue in error 72

Open briangmilnes opened this issue 1 year ago • 0 comments

// 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.

briangmilnes avatar Nov 08 '24 22:11 briangmilnes