SQLite lemma db and File lemma db cannot have some interface about keymaerax-release HOT 2 CLOSED

That means we should add a foreign key to the SQL table with the chosen identifier strings with a schema that says UNIQUE. Instead of or in addition to the auto-increment IDs?

Alternatively I wonder whether an improved version of the FileLemmaDB interface could work with existential types for LemmaID such that whatever is best can be used as identifiers. Albeit that might be a little annoying too. But certainly for micro-lemmas that merely store individual Provable steps, it's probably better to work with auto-incremented integer IDs, right @bbohrer ?

from keymaerax-release.

No change needed. Both databases guarantee unique IDs: the file lemma DB checks user-provided IDs for uniqueness; the SQLite lemma DB does not accept external IDs. User-generated IDs are inconvenient in the SQLite lemma DB (which stores proof steps but not user lemmas).

from keymaerax-release.