epfl-lara/lisa

It should be possible to export and import LISA proofs into and from text files.

SimonGuilloud opened this issue · 1 comments

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

We can do so into binary files with serialization since #187