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
