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
