Interleaving bug in the Language Server in Emacs

[briangmilnes]

/// Foo is not available in d'' called from d when c is missing.
module LangServerBug
val a : int -> int
val b : int -> int
val c : int -> int

let foo i = i < 1000000
val d : int -> int

module LangServerBug
let a i = i
let b i = i
(* let c i = i // intentionally left blank *)

let d'' (i:nat{foo i}) = i

let d (i:nat) = d'' i

Line breaks are required for this (otherwise dancing frog).

Compile as expected but the language server says:

Forge: VALIDATE _build/fstar/fst/checked/LangServerBug.fsti.checked
Forge: VALIDATE _build/fstar/fst/checked/LangServerBug.fst.checked

• Error 233 at src/fstar/fst/LangServerBug.fst(7,0-7,21):
  • Expected the definition of c to precede [d]

1 error was reported (see above)