Hello Everybody, I am working with FStar for a university project but do not have a lot of experience yet. Right now I'm struggling with a piece of code that typechecks just fine with fstar but when extracted throws type mismatch erros in ocaml.
A simplified example still showing the same behavior is: ``` module Test let main = let bt: Platform.Bytes.byte = 'A' in let bl: Platform.Bytes.bytes = FStar.Seq.of_list [bt; bt; bt] in let conn = Platform.Udp.connect "8.8.8.8" 53 in Platform.Udp.send conn bl ``` ocamlopt throws the following error: ``` File "out/Test.ml", line 6, characters 25-27: Error: This expression has type char FStar_Seq_Base.seq but an expression was expected of type Platform.Bytes.bytes ``` The extracted ocaml code (out/Test.ml) is: ``` open Prims let main : (Prims.string,Prims.unit) Platform.Error.optResult = let bt = 'A' in let bl = FStar_Seq_Base.of_list [bt; bt; bt] in let conn = Platform.Udp.connect "8.8.8.8" (Prims.parse_int "53") in Platform.Udp.send conn bl ``` I find this especially confusing since Platform.Bytes.bytes is defined as follows: ``` type bytes = Seq.seq byte ``` I am very grateful for any suggestions on whats going on! Regards, Frieder _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club