search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

fix universes in vector #1987

Closed Alizter closed 3 months ago

Alizter commented 3 months ago

With a little bit of help, we can get Coq to minimize the number of universes it uses for Vector.v.

jdchristensen commented 3 months ago

@Alizter Is this a duplicate of #1988?

Alizter commented 3 months ago

@jdchristensen Seems GitHub created two PRs due to my flaky internet connection. I've closed the other one.

Alizter commented 3 months ago

Thanks @jdchristensen, this appears to work better. I had a look and all the lemmas in Vector have the expected number of universes.