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

Change `ls_equal` implementation #380

Closed n-osborne closed 6 months ago

n-osborne commented 7 months ago

This PR proposes to move from physical equality to equality of the identifiers.

This will be needed as we plan to make gospel type checker modular (see #377): different files will be typed by different runs of the gospel program and physical equality won't hold between these runs.

n-osborne commented 6 months ago

Agree. Thanks :-)