search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Feature request: allow repetitions of definitions and theorems #140

Closed chaudhuri closed 1 year ago

chaudhuri commented 2 years ago

Currently we do not allow repetitions of Definitions and Theorems. This is causing various issues with the IPFS branch that are not worth getting into here.

Personally, I see no issue with allowing repetitions of definitions and theorems as long as they are identical.

(Issue arose in discussion with @innofarah.)

If we go this way, then one issue to consider is whether we use "identical" to mean "up to lambda-equivalence". For example, are the following two defintions identical?

Definition is_abs : tm -> prop by
  is_abs (abs R).

Definition is_abs : tm -> prop by
  is_abs (abs (x\ R x)).
chaudhuri commented 2 years ago

This feature could also obviate #133, perhaps.

chaudhuri commented 1 year ago

This is now implemented in the ipfs branch which may eventually be merged with master.