proof-extra with data rather than strings #607
Conversation
|
This will conflict with some of the changes I've made, but that's my fault for sitting on the s-expr PR for too long. I'll rebase it on top of this, I don't think the version of InferenceExtra I implemented is too different from this. |
|
Ah, you actually did something already! That's my fault, I should have communicated what I was doing - I just had a spare few hours today by some miracle. If it's easy to rebase go ahead, if not lmk and we can figure out what to do with it. |
|
@digama0 - I was quite pleased with this design until today, when we tried to use it and were told we can't @anjapetkovic and I will likely fix it together ("composition over inheritance" is the way to go, I expect) in the next few days so we can make progress on Dedukti. Let us know if you need something. |
|
I'll try to make a PR with my version of this thing. (I didn't use subtyping, I just had a discriminated union for |
We have started to receive interest in more proof outputs (e.g. Dedukti @anjapetkovic, Metamath @digama0) and these require a greater degree of granularity in proofs as they are machine-checked.
We already have
--proof_extra, but it's stringly-typed and hard to use for this purpose. Make explicit objects recording information about the proof for downstream use.While we're at it:
FREEoption. Happy to be persuaded.