search

UniMath / UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
http://unimath.org/
Other
960 stars 174 forks source link

UniMath rules - automatic verification #412

Open vladimirias opened 8 years ago

vladimirias commented 8 years ago

We need a script that can be included in the checks that a new contribution must pass before being accepted that verifies at least some of the rules.

To start with it can look for "Inductive", "Record" and other forbidden Coq commands.

It should also look for "Type" that must be replaced everywhere with UU or any other declared universe name. We will start do recover the universe discipline soon as Coq enables local "type-in-type".

I am not sure how it can control for the very important issue of re-definition of identifiers, but it should be possible to write one that will.

arnoudvanderleer commented 2 months ago

@rmatthes @benediktahrens @nmvdw Has this been solved in the last 7 years, by sanity-checks for example? Or do we need/like additional checks?

benediktahrens commented 2 months ago

No progress on this has been made, unfortunately.