search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
150 stars 31 forks source link

[petanque] New methods `state/eq` and `state/hash` #783

Closed ejgallego closed 3 months ago

ejgallego commented 3 months ago

This allows the client to implement a state hashtable; see the comments on the API for low-level details.

Note the changes in run result type. I have actually slightly refactored the type; @gbdrt please let me know if that's OK for you, or you would prefer the older type?

ejgallego commented 3 months ago

@gbdrt also please keep an eye on collisions once using this; I tuned the hashing function for document states, these could behave pretty different than proof states.