Hello, I’ve been trying out 0.9.4.3 from git, and in general am impressed with how F* is coming together. But the niceties of fstar-mode for Emacs really bring out the ugliness of its inferred types. For example, this definition of map
let rec map f l = match l with | [] -> [] | hd :: tl -> f hd :: map f tl Gave me this as a type Type f:(uu___182576:uu___182573 -> Prims.Tot uu___182572) -> l:Prims.list uu___182573 -> Prims.Tot (Prims.list uu___182572) I would have expected something a little more like f:(a0:ty1 -> Prims.Tot ty0) -> l:(Prims.list ty1) -> Prims.Tot (Prims.list ty0) Has anyone looked at making more readable gensyms? Having sensible prefixes and smaller counter values would help readability a lot. Cheers, Thomas
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club