FStar
FStar copied to clipboard
An interfaced module that references itself wrongly cause a dependency cycle
Test.fsti:
module Test
Test.fst:
module Test
let x:int = 0
let y:int = Test.x
$ fstar.exe Test.fst
* Error 117:
- You may have a cyclic dependence on module test: use --dep full to confirm. Alternatively, invoking fstar with Test.fst on the command line breaks the abstraction imposed by its interface Test.fsti; if you really want this behavior add the option '--expose_interfaces'
1 error was reported (see above)