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
