Hello Paul and Félix,
Thanks for the bug report -- I've filed
https://github.com/FStarLang/FStar/issues/1803
Out of curiosity, what was your initial interest in F*? Are you interested in
proving some numerical routines?
Cheers,
~ jonathan
From: fstar-club
Hi,
with Félix Breton (in cc) we get the following behaviour:
module Bug
open FStar.HyperStack.IO
module I32 = FStar.Int32
let main () =
if (I32.((-1l) <^ 0l)) then print_string "correct\n" else print_string
"wrong\n";
0
This prints "wrong", and was compiled
Hi Paul,
Don't think this duplication is useful for anything. Let's remove it:
https://github.com/FStarLang/FStar/pull/1801
Catalin
On Tue, Jul 2, 2019 at 10:45 AM paul zimmermann via fstar-club
wrote:
>
>Hi,
>
> on
>
Hi,
on
https://github.com/FStarLang/FStar/blob/master/INSTALL.md#building-f-from-sources,
paragraph "Instructions for all OSes", Step 4, in the line
$ opam install ocamlbuild ocamlfind ...,
the 'pprint' package is listed twice. Maybe this is wanted?
Best regards,
Paul Zimmermann
