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

Repeated Kind is OK, but repeated Type is not #139

Open chaudhuri opened 2 years ago

chaudhuri commented 2 years ago

As of 5bb9833e5655039740dadc56ad993f879c7e127b, Kind declarations can be repeated with no warnings or errors.

Kind n type.
Kind n type. % no issues

However, Type declarations cannot be repeated.

Type z n.
Type z n.

Error: Predicate or constant z already exists

Seems like an unintended discrepancy. Should perhaps be fixed by allowing redeclarations of Types as well.

(Issue spotted in discussion with @innofarah.)