search

IBM / AI-Descartes

Open source package for accelerated symbolic discovery of fundamental laws.
MIT License
105 stars 18 forks source link

Found: "Functions" at 10:1 Expected: ("ArchiveEntry" | "Lemma" | "Theorem" | "Exercise") Hint: Try ("ArchiveEntry" | "Lemma" | "Theorem" | "Exercise") #2

Open chuyanga opened 1 year ago

chuyanga commented 1 year ago

add: ArchiveEntry "" and Real abs( Real x ) =

corneliocristina commented 1 year ago

This error occurs with newer versions of KeYmaeraX. Try to use the version we recommend for the experiments: KeYmaeraX 4.9.3. You can download the right version from here). With more recent versions you need to modify the code (e.g. adding ArchiveEntry "entry_name" at the beginning of the KeYmaera files). See KeYmaeraX website for more details.