You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When reporting an error (in a newly opened split buffer, but this is probably a separate issue), fstar-mode includes the name of the most recently open'd module like this:
Example code, which causes an error due to the missing 't' at the end of "nat":
module Test
open FStar.Seq
type x = na
/home/kk/repositories/everest/FStar/ulib/FStar.Seq.Properties.fst(716,0-723,49): (Error) Identifier not found: [na](Also see: (5,9-5,11))] (FIXME)
Without opening FStar.Seq, the error is just
F*: subprocess exited.
(without openeing a split buffer). While running fstar.exe Test.fst from the command line just outputs:
./Test.fst(5,9-5,11) : (Error) Identifier not found: [na]
in both cases
Or maybe this is due to a configuration error on my part?
The text was updated successfully, but these errors were encountered:
When reporting an error (in a newly opened split buffer, but this is probably a separate issue), fstar-mode includes the name of the most recently
open
'd module like this:Example code, which causes an error due to the missing 't' at the end of "nat":
Without opening FStar.Seq, the error is just
(without openeing a split buffer). While running
fstar.exe Test.fst
from the command line just outputs:in both cases
Or maybe this is due to a configuration error on my part?
The text was updated successfully, but these errors were encountered: