Add LSP command to add DEFs to a leaf proof for ExpandENABLED to work.

tlaplus / tlapm

The TLA Proof Manager

https://proofs.tlapl.us/

BSD 2-Clause "Simplified" License

67 stars 20 forks source link

Open kape1395 opened 1 month ago

kape1395 commented 1 month ago

This could replace the AutoUSE directive.

lemmy commented 1 month ago

It could also be interesting to see how well e.g. Github Copilot is able to predict those defs.

kape1395 commented 1 month ago

@vleveris, can you check this?

It could also be interesting to see how well e.g. Github Copilot is able to predict those defs.