It should be possible to export and import LISA proofs into and from text files.
SimonGuilloud opened this issue · 1 comments
SimonGuilloud commented
It should be possible to export LISA's kernel proof unambiguously to text files, and import them back
Suggested format:
#2 |- A => A by Subproof with -1, -3 {
#2.-2 X by Import
#2.-1 Y by Import
#2.0 Z by LeftImplies with A
}
#3 |- B by Cut 0, 1 with phi
SimonGuilloud commented
We can do so into binary files with serialization since #187