Skip to content

Multiple changes to the running theories

Viktor Kuncak requested to merge github/fork/SimonGuilloud/main into main

Created by: SimonGuilloud

  • Theorems and Axioms are now stored with a name and can be fetched using that name. Definitions can be fetched using the symbol that they define.
  • When trying to convert a proof to a theorem or to get a definition, the user is returned a meaningfull error message indicating what went wrong.
  • Corrected an unsoundness that permitted to define a symbol in terms of an unbound variable or a schematic symbol.

Merge request reports