Hi Jonathan, Thanks for the reply. I have filed the bug in the github issues.
Best, Zhiting On Fri, May 5, 2017 at 7:47 AM, Jonathan Protzenko <pr...@microsoft.com> wrote: > HI Zhiting, > > > This is a use-case that no one has ever exercised so far, meaning that the > translation is lacking. Can you file a bug at https://github.com/ > FStarLang/kremlin/issues? I'd be more than happy to take a look at it. > > > Thanks, > > > ~ jonathan > ------------------------------ > *From:* fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf > of zhiting zhu via fstar-club <fstar-club@lists.gforge.inria.fr> > *Sent:* Thursday, May 4, 2017 12:13:02 PM > *To:* fstar-club@lists.gforge.inria.fr > *Subject:* [fstar-club] kremlin question: define struct > > Hi, > > I wonder whether there's any way to define a type that would translate to > struct similar to the following form: > > typedef struct { > int32_t x01; > struct t* x10; > } > t; > > I have tried to use > > type t = > | T: Int32.t -> Buffer.buffer t -> t > > But what this translates to is > > typedef struct { > int32_t x01; > t* x10; > } > t; > which does not work for C. > > Thanks, > Zhiting >
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
