Gospel does not parse `fun` type annotations as OCaml
Closed this issue · 2 comments
shym commented
The following code is accepted by the OCaml type checker:
fun true : int -> 12
(besides the obviously non-exhaustive pattern true
), meaning that the int
is the return type but the Gospel typechecker accepts the following:
val f : int list -> int
(*@ y = f xs
ensures List.for_all (fun x : int -> true) xs *)
where int
is interpreted as the type for the argument x
.