search

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
123 stars 16 forks source link

Records with partially same fields name #415

Open n-osborne opened 1 month ago

n-osborne commented 1 month ago

Running Gospel type-checker on this file:

(*@ type t = { a: bool; b: integer } *)
(*@ type r = { a: bool; c: integer } *)

val f : int -> bool
(*@ ensures let x = { a = true; b = 42 } in true *)

fails with:

File "/tmp/bob.mli", line 5, characters 20-40:
5 | (*@ ensures let x = { a = true; b = 42 } in true *)
                        ^^^^^^^^^^^^^^^^^^^^
Error: The record field b does not exist.