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
