FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Qualifiers are sensitive to ordering

Open R1kM opened this issue 10 months ago • 0 comments

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.

R1kM avatar Apr 04 '24 14:04 R1kM