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 <catalin.hri...@gmail.com> > Date: Mon, 16 Mar 2020 16:30:00 +0100 > Cc: Jonathan Protzenko <pr...@microsoft.com>, FStar Club > <fstar-club@lists.gforge.inria.fr>, > Guido Martinez <mtzgu...@gmail.com> > > 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 at 8:04 AM paul zimmermann via fstar-club > <fstar-club@lists.gforge.inria.fr> wrote: > > > > Dear Jonathan, > > > > > From: Jonathan Protzenko <pr...@microsoft.com> > > > Date: Wed, 3 Jul 2019 05:30:37 +0000 > > > > > > 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 > > > > thank you. We try to prove some routines from the GNU MPFR library, > > following work started by Jianyang Pan last year, with the help of Karthik. > > > > Best regards, > > Paul Zimmermann > > _______________________________________________ > > fstar-club mailing list > > fstar-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/fstar-club _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
