Hi everyone,
I'm just playing a bit around with F-Star and Kremlin and I seem to be stuck at
a simple problem. I don't know if I'm missing something obvious or if this
might be a bug. My code looks like this:
let main () =
C.print_string (C.string_of_literal (String.concat ", " (List.Tot.map
string_of_int [1; 2; 3])));
C.exit_success
I expect this code to print `1, 2, 3` but instead I get the following runtime
error:
KreMLin abort at ./Main.c:9
This function was not extracted:
Failure("Cannot extract string_of_literal applied to a non-literal")
I tried some variations of the above program to see if I can reverse-engineer
what is going on, but as soon as I introduce `List.Tot.map`, the code breaks. I
know that there is also `C.Loops.map`, but I don't know if I really need to use
buffers to make it work.
Also, I'm generally interested in learning more about Kremlin / Low* / F*. If
there are any recommended resources or other helpful links, feel free to share
them with me.
Thank you and best regards,
--
Pierre Beaucamp
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
