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
$ ./bin/fstar.exe BB.fst
* Warning 241 at AA.fst(0,0-0,0):
- Unable to load AA.fst.checked since checked file AA.fst.checked does not
exist; will recheck AA.fst (suppressing this warning for further modules)
* Error 134 at BB.fst(3,5-3,7):
- Namespace AA cannot be found
1 error was reported (see above)
The first warning is expected. The second error does not mention a missing file, so it did find AA.fst and loaded it, but its name had a wrong case, so the AA namespace/module is not present, only Aa is.
The text was updated successfully, but these errors were encountered:
Trying to check
BB
gives:The first warning is expected. The second error does not mention a missing file, so it did find
AA.fst
and loaded it, but its name had a wrong case, so theAA
namespace/module is not present, onlyAa
is.The text was updated successfully, but these errors were encountered: