Dear Catalin,
thank you for the information. We are no longer working on this at the moment,
but in case we resume it will be very useful!
Best regards,
Paul
> From: Catalin Hritcu
> Date: Mon, 16 Mar 2020 16:30:00 +0100
> Cc: Jonathan Protzenko , FStar Club
> ,
> Guido Martinez
Dear Paul and Felix,
Guido has just fixed https://github.com/FStarLang/FStar/issues/1803
by doing a big cleanup to the way we do machine integers in F*:
https://github.com/FStarLang/FStar/pull/1850
Please have another look and sorry for the inconvenience.
Regards,
Catalin
On Wed, Jul 3, 2019
Dear Jonathan,
> From: Jonathan Protzenko
> Date: Wed, 3 Jul 2019 05:30:37 +
>
> 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
>
on behalf of paul
zimmermann via fstar-club
Sent: Tuesday, July 2, 2019 7:33 AM
To: fstar-club@lists.gforge.inria.fr
Cc: felix.bre...@inria.fr
Subject: [fstar-club] bug report (wrong cast from I32)
Hi,
with Félix Breton (in cc) we get the following behaviour:
module Bug
open
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
