I've split LDL_function.v into multiple files, ldl.v containing the logic and translations, goedel.vdl2.v and stl.v containing the respective theories.
I've also removed old files and the ITP draft, since we have a separate repository to track that.
Shadow lifting does not work, so it's commented out for now, maybe it's something that @affeldt-aist can take a look at.
Update: this also adds an alternative formulation of STL without infinities that can be found in stlalt.v
I've split
LDL_function.vinto multiple files,ldl.vcontaining the logic and translations,goedel.vdl2.vandstl.vcontaining the respective theories. I've also removed old files and the ITP draft, since we have a separate repository to track that. Shadow lifting does not work, so it's commented out for now, maybe it's something that @affeldt-aist can take a look at. Update: this also adds an alternative formulation of STL without infinities that can be found instlalt.v