Feature idea
When writing a proof, I sometimes prove the same goal multiple times (often something about indices being inside the correct bounds).
Would there be a way to store this proof in the context as an hypothesis so that when it is relevant the proof could be reused, maybe even as a // ?
The idea is that if \phi => p then for any \delta, \phi U \delta => p. Storing that there is a proof of \phi => p for a minimal p could simplify writing (speedup verifying ?) the proofs.
It sounds equivalent to writing a have h : p by proof and being able to apply h.
Maybe introduce a new keyword remember to indicate that the proof of the current goal should be stored to be reused.
Feature idea
When writing a proof, I sometimes prove the same goal multiple times (often something about indices being inside the correct bounds).
Would there be a way to store this proof in the context as an hypothesis so that when it is relevant the proof could be reused, maybe even as a
//?The idea is that if
\phi => pthenfor any \delta, \phi U \delta => p. Storing that there is a proof of\phi => pfor a minimalpcould simplify writing (speedup verifying ?) the proofs.It sounds equivalent to writing a
have h : p by proofand being able toapply h.Maybe introduce a new keyword
rememberto indicate that the proof of the current goal should be stored to be reused.