search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Move export SetTheoryLibrary.* from Main to proof files #33

Closed cache-nez closed 2 years ago

cache-nez commented 2 years ago

Let Main be responsible for output-related functionality, this way it can be reused for other theories, e.g. the Peano arithmetic that is under development.

SimonGuilloud commented 2 years ago

No, the main library is based on set theory. It's a defining feature of LISA. While the kernel supports different theories on principle, and could be used to develop others, we definitely don't want to handle multiple theories. Someday it could be like Isabelle/HOL and Isabelle/ZF, but we're not there yet. Those particular files here are fully intended to be used as a main library in the main set theory and it is a feature that they should include the specific theory. This is the setting where you are supposed to define peano arithmetic.

cache-nez commented 2 years ago

This is the setting where you are supposed to define peano arithmetic.

I'm not sure I follow this. Are you saying Peano arithmetic should be defined as an extension of set theory?