FStar
FStar copied to clipboard
Qualifiers are sensitive to ordering
Consider the following code:
module Test
inline_for_extraction noextract
val f (x:int) : unit
noextract inline_for_extraction
let f x = ()
Attempting to typecheck currently raises the following error
(Error 93) - Inconsistent qualifier annotations on f
- Expected 'inline_for_extraction noextract'
got 'noextract inline_for_extraction'
Ideally, the order of qualifiers would not matter, the only requirement should be that the sets match.