Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.
Already on GitHub?
to your account
In 2.3.2 of the tutorial there is a simple example every ML user is familiar with:
val new_counter: int -> St (unit -> St int)
let new_counter (start: int) =
let c = ST.alloc start in
fun () -> c := !c + 1; !c
However, F* is not able to verify this example, throwing the error:
(Error) Failed to resolve implicit argument of type 'FStar.Preorder.preorder ((fun start -> (fun start -> (fun start -> (fun start -> Prims.int) start) start) start) start)' introduced in (*?u41*) _ start (see also Eff2(9,25-9,27))
The text was updated successfully, but these errors were encountered:
Good to see you around here :)
This is already tracked in #1056, which has a fix for that inference failure. However, the example has an assertion failure which I'm not sure has had a proper diagnosis.
In general, the tutorial usually lags behind development as we don't yet have a way to automatically test it.
Sorry, something went wrong.
Hi! The assertion failure is due to the imprecise encoding of impure arrows to the smt solver (#855). I need to fix it soon.
Regarding the inference failure, we should change the tutorial to use open FStar.Ref instead of open FStar.ST. This is also logged in the README here: https://github.com/FStarLang/FStar/blob/master/CHANGES.md (the second bullet under Standard Library).
Closing as duplicate
Successfully merging a pull request may close this issue.