search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Remove mutability from theorem proof field #1307

Closed digama0 closed 2 months ago

digama0 commented 2 months ago

The original code was using a proof ref in every theorem just for deletion, but every use was already in a position to pass a modified theorem back, so doing that saves an indirection and additional state.

mn200 commented 2 months ago

I assume the static error in build-otknl will be an easy fix?

digama0 commented 2 months ago

Actually, I think this won't work. The issue is that proofs can be deleted after the fact via directives in the .otd file, after the theorem has already been referenced in several other theorems. This will need another implementation, and I don't think it's worth it since this is opentheory-specific behavior.